acsl

    3熱度

    1回答

    可能無限C函數的ACSL規範

    我想指定外部函數的行爲，更準確地說，它們的終止。 ACSL文檔指出\terminates p;屬性指定如果謂詞p成立，則保證該函數終止，但在p不成立時指定任何內容。這也解釋了從不返回的函數可以通過指定： //@ ensures \false ; terminates \false ; 而且ACSL提供財產\exits p;指定在突然終止的情況下，後置條件。所以我想知道是否： //@ ensur
    frama-c language-specifications acsl 2013-02-21

    3熱度

    1回答

    如何在frama-c中調試ACSL？

    我在努力學習ACSL，但是試圖編寫一個完整的規範時磕磕絆絆。我的代碼 #include <stdint.h> #include <stddef.h> #define NUM_ELEMS (8) /*@ requires expected != test; @ requires \let n = NUM_ELEMS; @ \valid_read(expected +
    frama-c acsl 2017-07-19

    0熱度

    2回答

    如何強制內存位置在ACSL中有效？

    我定義設備訪問如從而 volatile struct mydevice * const dev = (struct mydevice *)MY_DEVICE_ADDRESS; 我建模使用 @ volatile dev->somereg reads somereg_read writes somereg_write; 現在的問題是，當我使RTE檢查，所產生的有效性檢查不能證明的訪問 /*@
    frama-c acsl 2017-07-20

    0熱度

    2回答

    ACSL位串閃爍

    我需要有關ACSL問題的幫助。比賽在2014-2015年完成。這只是練習，我想看看我是否正確地解決了這個問題。 位串輕拂： 求解下面的方程x（5個比特）。有多少獨特的解決方案？ （RCIRC-2（LSHIFT-1（NOT X）））= 00101 解決我得到了16個獨特的解決方案，雖然我不能在任何地方找到答案，需要你的幫助智能和後有創意的人！ 感謝
    bitstring acsl 2016-02-02

    2熱度

    1回答

    ACSL「分配」註解爲內結構和的C代碼字段

    假設我們有這樣的數據結構： #typedef struct { int C_Field; }C; #typedef struct { C B_Array[MAX_SIZE]; }B; #typedef struct { B A_Array[MAX_SIZE]; }A; 似乎郵資-C不爲一個結構的一個字段分配一個位置在以下示例中鍵入C： /*@ assigns
    static-analysis frama-c acsl 2017-04-27

    -3熱度

    1回答

    需要關於2013年以前的acsl計劃的幫助

    我的老師讓我們做一個老練的ACSL計劃，他說我們可以使用我們想要的任何資源。該計劃是從2013年開始請點這裏：https://s3.amazonaws.com/iedu-attachments-question/5a989d787772b7fd88c063aff8393d34_1bee2d300c35eec13edf0a3af515a5a5.pdf 我們啓動的程序，但我們撞上了牆，我們不知道該怎麼
    python acsl 2016-02-06
最新問題