Skip to content
Snippets Groups Projects
Commit b2256999 authored by Julien Signoles's avatar Julien Signoles
Browse files

updating tests for farm-lsl-cloud

parent b1f8150d
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 1316 additions and 1316 deletions
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
+ 1
− 1
View file @ b2256999
......@@ -2,7 +2,7 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
PROJECT_FILE.i:136:[value] Assertion got status valid.
PROJECT_FILE.i:200:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
+ 12
− 12
View file @ b2256999
......@@ -8,29 +8,29 @@ tests/e-acsl-runtime/array.i:14:[e-acsl] warning: missing guard for ensuring tha
[value] Values of globals at initialization
T1[0..2] ∈ {0}
T2[0..3] ∈ {0}
PROJECT_FILE.i:138:[value] entering loop for the first time
PROJECT_FILE.i:142:[value] assigning non deterministic value for the first time
PROJECT_FILE.i:147:[value] entering loop for the first time
PROJECT_FILE.i:154:[value] Assertion got status unknown.
PROJECT_FILE.i:202:[value] entering loop for the first time
PROJECT_FILE.i:206:[value] assigning non deterministic value for the first time
PROJECT_FILE.i:211:[value] entering loop for the first time
PROJECT_FILE.i:218:[value] Assertion got status unknown.
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:155.
Called from PROJECT_FILE.i:219.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
PROJECT_FILE.i:119:[value] Function exit: postcondition got status invalid.
Called from PROJECT_FILE.i:193.
PROJECT_FILE.i:183:[value] Function exit: postcondition got status invalid.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
PROJECT_FILE.i:157:[value] Assertion got status unknown.
PROJECT_FILE.i:221:[value] Assertion got status unknown.
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:158.
Called from PROJECT_FILE.i:222.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
+ 19
− 19
View file @ b2256999
......@@ -4,50 +4,50 @@ tests/e-acsl-runtime/cast.i:18:[e-acsl] warning: missing guard for ensuring that
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
PROJECT_FILE.i:138:[value] Assertion got status valid.
PROJECT_FILE.i:202:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_str <- main.
Called from PROJECT_FILE.i:142.
PROJECT_FILE.i:37:[value] Function __gmpz_init_set_str: postcondition got status valid.
Called from PROJECT_FILE.i:206.
PROJECT_FILE.i:79:[value] Function __gmpz_init_set_str: postcondition got status valid.
[value] Done for function __gmpz_init_set_str
[value] computing for function __gmpz_get_si <- main.
Called from PROJECT_FILE.i:143.
PROJECT_FILE.i:96:[value] Function __gmpz_get_si: precondition got status valid.
Called from PROJECT_FILE.i:207.
PROJECT_FILE.i:138:[value] Function __gmpz_get_si: precondition got status valid.
[value] Done for function __gmpz_get_si
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:144.
Called from PROJECT_FILE.i:208.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
PROJECT_FILE.i:119:[value] Function exit: postcondition got status invalid.
Called from PROJECT_FILE.i:193.
PROJECT_FILE.i:183:[value] Function exit: postcondition got status invalid.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:145.
PROJECT_FILE.i:43:[value] Function __gmpz_clear: precondition got status valid.
Called from PROJECT_FILE.i:209.
PROJECT_FILE.i:85:[value] Function __gmpz_clear: precondition got status valid.
[value] Done for function __gmpz_clear
PROJECT_FILE.i:149:[value] Assertion got status valid.
PROJECT_FILE.i:213:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_str <- main.
Called from PROJECT_FILE.i:153.
Called from PROJECT_FILE.i:217.
[value] Done for function __gmpz_init_set_str
[value] computing for function __gmpz_get_ui <- main.
Called from PROJECT_FILE.i:154.
PROJECT_FILE.i:100:[value] Function __gmpz_get_ui: precondition got status valid.
Called from PROJECT_FILE.i:218.
PROJECT_FILE.i:142:[value] Function __gmpz_get_ui: precondition got status valid.
[value] Done for function __gmpz_get_ui
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:156.
Called from PROJECT_FILE.i:220.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:158.
Called from PROJECT_FILE.i:222.
[value] Done for function __gmpz_clear
[value] Recording results for main
[value] done for function main
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
+ 106
− 106
View file @ b2256999
......@@ -2,279 +2,279 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
PROJECT_FILE.i:139:[value] Assertion got status valid.
PROJECT_FILE.i:142:[value] Assertion got status valid.
PROJECT_FILE.i:145:[value] Assertion got status valid.
PROJECT_FILE.i:203:[value] Assertion got status valid.
PROJECT_FILE.i:206:[value] Assertion got status valid.
PROJECT_FILE.i:209:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:150.
PROJECT_FILE.i:33:[value] Function __gmpz_init_set_si: postcondition got status valid.
Called from PROJECT_FILE.i:214.
PROJECT_FILE.i:75:[value] Function __gmpz_init_set_si: postcondition got status valid.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:151.
Called from PROJECT_FILE.i:215.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:152.
PROJECT_FILE.i:49:[value] Function __gmpz_cmp: precondition got status valid.
PROJECT_FILE.i:50:[value] Function __gmpz_cmp: precondition got status valid.
Called from PROJECT_FILE.i:216.
PROJECT_FILE.i:91:[value] Function __gmpz_cmp: precondition got status valid.
PROJECT_FILE.i:92:[value] Function __gmpz_cmp: precondition got status valid.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:153.
Called from PROJECT_FILE.i:217.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
PROJECT_FILE.i:119:[value] Function exit: postcondition got status invalid.
Called from PROJECT_FILE.i:193.
PROJECT_FILE.i:183:[value] Function exit: postcondition got status invalid.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:154.
PROJECT_FILE.i:43:[value] Function __gmpz_clear: precondition got status valid.
Called from PROJECT_FILE.i:218.
PROJECT_FILE.i:85:[value] Function __gmpz_clear: precondition got status valid.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:155.
Called from PROJECT_FILE.i:219.
[value] Done for function __gmpz_clear
PROJECT_FILE.i:159:[value] Assertion got status valid.
PROJECT_FILE.i:223:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:164.
Called from PROJECT_FILE.i:228.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:165.
Called from PROJECT_FILE.i:229.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:166.
Called from PROJECT_FILE.i:230.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:167.
Called from PROJECT_FILE.i:231.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:168.
Called from PROJECT_FILE.i:232.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:169.
Called from PROJECT_FILE.i:233.
[value] Done for function __gmpz_clear
PROJECT_FILE.i:174:[value] Assertion got status valid.
PROJECT_FILE.i:177:[value] Assertion got status unknown.
PROJECT_FILE.i:180:[value] Assertion got status valid.
PROJECT_FILE.i:183:[value] Assertion got status valid.
PROJECT_FILE.i:186:[value] Assertion got status valid.
PROJECT_FILE.i:189:[value] Assertion got status valid.
PROJECT_FILE.i:192:[value] Assertion got status valid.
PROJECT_FILE.i:195:[value] Assertion got status valid.
PROJECT_FILE.i:198:[value] Assertion got status valid.
PROJECT_FILE.i:238:[value] Assertion got status valid.
PROJECT_FILE.i:241:[value] Assertion got status unknown.
PROJECT_FILE.i:244:[value] Assertion got status valid.
PROJECT_FILE.i:247:[value] Assertion got status valid.
PROJECT_FILE.i:250:[value] Assertion got status valid.
PROJECT_FILE.i:253:[value] Assertion got status valid.
PROJECT_FILE.i:256:[value] Assertion got status valid.
PROJECT_FILE.i:259:[value] Assertion got status valid.
PROJECT_FILE.i:262:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:204.
Called from PROJECT_FILE.i:268.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
Called from PROJECT_FILE.i:205.
PROJECT_FILE.i:21:[value] Function __gmpz_init: postcondition got status valid.
Called from PROJECT_FILE.i:269.
PROJECT_FILE.i:63:[value] Function __gmpz_init: postcondition got status valid.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_neg <- main.
Called from PROJECT_FILE.i:206.
PROJECT_FILE.i:59:[value] Function __gmpz_neg: precondition got status valid.
PROJECT_FILE.i:60:[value] Function __gmpz_neg: precondition got status valid.
Called from PROJECT_FILE.i:270.
PROJECT_FILE.i:101:[value] Function __gmpz_neg: precondition got status valid.
PROJECT_FILE.i:102:[value] Function __gmpz_neg: precondition got status valid.
[value] Done for function __gmpz_neg
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:207.
Called from PROJECT_FILE.i:271.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:208.
Called from PROJECT_FILE.i:272.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:209.
Called from PROJECT_FILE.i:273.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:210.
Called from PROJECT_FILE.i:274.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:211.
Called from PROJECT_FILE.i:275.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:212.
Called from PROJECT_FILE.i:276.
[value] Done for function __gmpz_clear
PROJECT_FILE.i:216:[value] Assertion got status valid.
PROJECT_FILE.i:280:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:222.
Called from PROJECT_FILE.i:286.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:223.
Called from PROJECT_FILE.i:287.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
Called from PROJECT_FILE.i:224.
Called from PROJECT_FILE.i:288.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_neg <- main.
Called from PROJECT_FILE.i:225.
Called from PROJECT_FILE.i:289.
[value] Done for function __gmpz_neg
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:226.
Called from PROJECT_FILE.i:290.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:227.
Called from PROJECT_FILE.i:291.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:228.
Called from PROJECT_FILE.i:292.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:229.
Called from PROJECT_FILE.i:293.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:230.
Called from PROJECT_FILE.i:294.
[value] Done for function __gmpz_clear
PROJECT_FILE.i:234:[value] Assertion got status valid.
PROJECT_FILE.i:298:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:240.
Called from PROJECT_FILE.i:304.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
Called from PROJECT_FILE.i:241.
Called from PROJECT_FILE.i:305.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_neg <- main.
Called from PROJECT_FILE.i:242.
Called from PROJECT_FILE.i:306.
[value] Done for function __gmpz_neg
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:243.
Called from PROJECT_FILE.i:307.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:244.
Called from PROJECT_FILE.i:308.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:245.
Called from PROJECT_FILE.i:309.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:246.
Called from PROJECT_FILE.i:310.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:247.
Called from PROJECT_FILE.i:311.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:248.
Called from PROJECT_FILE.i:312.
[value] Done for function __gmpz_clear
PROJECT_FILE.i:252:[value] Assertion got status valid.
PROJECT_FILE.i:316:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:258.
Called from PROJECT_FILE.i:322.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:259.
Called from PROJECT_FILE.i:323.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
Called from PROJECT_FILE.i:260.
Called from PROJECT_FILE.i:324.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_neg <- main.
Called from PROJECT_FILE.i:261.
Called from PROJECT_FILE.i:325.
[value] Done for function __gmpz_neg
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:262.
Called from PROJECT_FILE.i:326.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:263.
Called from PROJECT_FILE.i:327.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:264.
Called from PROJECT_FILE.i:328.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:265.
Called from PROJECT_FILE.i:329.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:266.
Called from PROJECT_FILE.i:330.
[value] Done for function __gmpz_clear
PROJECT_FILE.i:270:[value] Assertion got status valid.
PROJECT_FILE.i:334:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:275.
Called from PROJECT_FILE.i:339.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
Called from PROJECT_FILE.i:276.
Called from PROJECT_FILE.i:340.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_neg <- main.
Called from PROJECT_FILE.i:277.
Called from PROJECT_FILE.i:341.
[value] Done for function __gmpz_neg
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:278.
Called from PROJECT_FILE.i:342.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:279.
Called from PROJECT_FILE.i:343.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:280.
Called from PROJECT_FILE.i:344.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:281.
Called from PROJECT_FILE.i:345.
[value] Done for function __gmpz_clear
PROJECT_FILE.i:285:[value] Assertion got status valid.
PROJECT_FILE.i:349:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:291.
Called from PROJECT_FILE.i:355.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:292.
Called from PROJECT_FILE.i:356.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
Called from PROJECT_FILE.i:293.
Called from PROJECT_FILE.i:357.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_neg <- main.
Called from PROJECT_FILE.i:294.
Called from PROJECT_FILE.i:358.
[value] Done for function __gmpz_neg
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:295.
Called from PROJECT_FILE.i:359.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:296.
Called from PROJECT_FILE.i:360.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:297.
Called from PROJECT_FILE.i:361.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:298.
Called from PROJECT_FILE.i:362.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:299.
Called from PROJECT_FILE.i:363.
[value] Done for function __gmpz_clear
[value] Recording results for main
[value] done for function main
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
+ 14
− 14
View file @ b2256999
......@@ -2,32 +2,32 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
PROJECT_FILE.i:135:[value] Assertion got status valid.
PROJECT_FILE.i:139:[value] Assertion got status valid.
PROJECT_FILE.i:142:[value] Assertion got status valid.
PROJECT_FILE.i:199:[value] Assertion got status valid.
PROJECT_FILE.i:203:[value] Assertion got status valid.
PROJECT_FILE.i:206:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_str <- main.
Called from PROJECT_FILE.i:146.
PROJECT_FILE.i:37:[value] Function __gmpz_init_set_str: postcondition got status valid.
Called from PROJECT_FILE.i:210.
PROJECT_FILE.i:79:[value] Function __gmpz_init_set_str: postcondition got status valid.
[value] Done for function __gmpz_init_set_str
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:147.
PROJECT_FILE.i:49:[value] Function __gmpz_cmp: precondition got status valid.
PROJECT_FILE.i:50:[value] Function __gmpz_cmp: precondition got status valid.
Called from PROJECT_FILE.i:211.
PROJECT_FILE.i:91:[value] Function __gmpz_cmp: precondition got status valid.
PROJECT_FILE.i:92:[value] Function __gmpz_cmp: precondition got status valid.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:149.
Called from PROJECT_FILE.i:213.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
PROJECT_FILE.i:119:[value] Function exit: postcondition got status invalid.
Called from PROJECT_FILE.i:193.
PROJECT_FILE.i:183:[value] Function exit: postcondition got status invalid.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:151.
PROJECT_FILE.i:43:[value] Function __gmpz_clear: precondition got status valid.
Called from PROJECT_FILE.i:215.
PROJECT_FILE.i:85:[value] Function __gmpz_clear: precondition got status valid.
[value] Done for function __gmpz_clear
[value] Recording results for main
[value] done for function main
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
+ 72
− 72
View file @ b2256999
......@@ -2,194 +2,194 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
PROJECT_FILE.i:138:[value] Assertion got status valid.
PROJECT_FILE.i:202:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:144.
PROJECT_FILE.i:33:[value] Function __gmpz_init_set_si: postcondition got status valid.
Called from PROJECT_FILE.i:208.
PROJECT_FILE.i:75:[value] Function __gmpz_init_set_si: postcondition got status valid.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:145.
Called from PROJECT_FILE.i:209.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:146.
PROJECT_FILE.i:49:[value] Function __gmpz_cmp: precondition got status valid.
PROJECT_FILE.i:50:[value] Function __gmpz_cmp: precondition got status valid.
Called from PROJECT_FILE.i:210.
PROJECT_FILE.i:91:[value] Function __gmpz_cmp: precondition got status valid.
PROJECT_FILE.i:92:[value] Function __gmpz_cmp: precondition got status valid.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:151.
Called from PROJECT_FILE.i:215.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:152.
Called from PROJECT_FILE.i:216.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:153.
Called from PROJECT_FILE.i:217.
[value] Done for function __gmpz_cmp
PROJECT_FILE.i:154:[value] assigning non deterministic value for the first time
PROJECT_FILE.i:218:[value] assigning non deterministic value for the first time
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:155.
PROJECT_FILE.i:43:[value] Function __gmpz_clear: precondition got status valid.
Called from PROJECT_FILE.i:219.
PROJECT_FILE.i:85:[value] Function __gmpz_clear: precondition got status valid.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:156.
Called from PROJECT_FILE.i:220.
[value] Done for function __gmpz_clear
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:159.
Called from PROJECT_FILE.i:223.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
PROJECT_FILE.i:119:[value] Function exit: postcondition got status invalid.
Called from PROJECT_FILE.i:193.
PROJECT_FILE.i:183:[value] Function exit: postcondition got status invalid.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:160.
Called from PROJECT_FILE.i:224.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:161.
Called from PROJECT_FILE.i:225.
[value] Done for function __gmpz_clear
PROJECT_FILE.i:165:[value] Assertion got status valid.
PROJECT_FILE.i:229:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:171.
Called from PROJECT_FILE.i:235.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:172.
Called from PROJECT_FILE.i:236.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:173.
Called from PROJECT_FILE.i:237.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:179.
Called from PROJECT_FILE.i:243.
[value] Done for function __gmpz_init_set_si
PROJECT_FILE.i:180:[value] Assertion got status invalid (stopping propagation).
PROJECT_FILE.i:244:[value] Assertion got status invalid (stopping propagation).
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:191.
Called from PROJECT_FILE.i:255.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:192.
Called from PROJECT_FILE.i:256.
[value] Done for function __gmpz_clear
PROJECT_FILE.i:196:[value] Assertion got status valid.
PROJECT_FILE.i:260:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:202.
Called from PROJECT_FILE.i:266.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:203.
Called from PROJECT_FILE.i:267.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:204.
Called from PROJECT_FILE.i:268.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:210.
Called from PROJECT_FILE.i:274.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:211.
Called from PROJECT_FILE.i:275.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:212.
Called from PROJECT_FILE.i:276.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:214.
Called from PROJECT_FILE.i:278.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:215.
Called from PROJECT_FILE.i:279.
[value] Done for function __gmpz_clear
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:217.
Called from PROJECT_FILE.i:281.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:218.
Called from PROJECT_FILE.i:282.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:219.
Called from PROJECT_FILE.i:283.
[value] Done for function __gmpz_clear
PROJECT_FILE.i:223:[value] Assertion got status valid.
PROJECT_FILE.i:287:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:229.
Called from PROJECT_FILE.i:293.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:230.
Called from PROJECT_FILE.i:294.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:231.
Called from PROJECT_FILE.i:295.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:238.
Called from PROJECT_FILE.i:302.
[value] Done for function __gmpz_init_set_si
PROJECT_FILE.i:239:[value] Assertion got status invalid (stopping propagation).
PROJECT_FILE.i:303:[value] Assertion got status invalid (stopping propagation).
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:249.
Called from PROJECT_FILE.i:313.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:250.
Called from PROJECT_FILE.i:314.
[value] Done for function __gmpz_clear
PROJECT_FILE.i:254:[value] Assertion got status valid.
PROJECT_FILE.i:318:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:260.
Called from PROJECT_FILE.i:324.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:261.
Called from PROJECT_FILE.i:325.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:262.
Called from PROJECT_FILE.i:326.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:268.
Called from PROJECT_FILE.i:332.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:269.
Called from PROJECT_FILE.i:333.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:270.
Called from PROJECT_FILE.i:334.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:272.
Called from PROJECT_FILE.i:336.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:273.
Called from PROJECT_FILE.i:337.
[value] Done for function __gmpz_clear
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:275.
Called from PROJECT_FILE.i:339.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:276.
Called from PROJECT_FILE.i:340.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:277.
Called from PROJECT_FILE.i:341.
[value] Done for function __gmpz_clear
PROJECT_FILE.i:281:[value] Assertion got status valid.
PROJECT_FILE.i:345:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:287.
Called from PROJECT_FILE.i:351.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:288.
Called from PROJECT_FILE.i:352.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:289.
Called from PROJECT_FILE.i:353.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:296.
Called from PROJECT_FILE.i:360.
[value] Done for function __gmpz_init_set_si
PROJECT_FILE.i:297:[value] Assertion got status invalid (stopping propagation).
PROJECT_FILE.i:361:[value] Assertion got status invalid (stopping propagation).
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:307.
Called from PROJECT_FILE.i:371.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:308.
Called from PROJECT_FILE.i:372.
[value] Done for function __gmpz_clear
[value] Recording results for main
[value] done for function main
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
+ 54
− 54
View file @ b2256999
......@@ -2,161 +2,161 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
PROJECT_FILE.i:138:[value] Assertion got status valid.
PROJECT_FILE.i:202:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:151.
PROJECT_FILE.i:33:[value] Function __gmpz_init_set_si: postcondition got status valid.
Called from PROJECT_FILE.i:215.
PROJECT_FILE.i:75:[value] Function __gmpz_init_set_si: postcondition got status valid.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:152.
Called from PROJECT_FILE.i:216.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:153.
PROJECT_FILE.i:49:[value] Function __gmpz_cmp: precondition got status valid.
PROJECT_FILE.i:50:[value] Function __gmpz_cmp: precondition got status valid.
Called from PROJECT_FILE.i:217.
PROJECT_FILE.i:91:[value] Function __gmpz_cmp: precondition got status valid.
PROJECT_FILE.i:92:[value] Function __gmpz_cmp: precondition got status valid.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:154.
Called from PROJECT_FILE.i:218.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
PROJECT_FILE.i:119:[value] Function exit: postcondition got status invalid.
Called from PROJECT_FILE.i:193.
PROJECT_FILE.i:183:[value] Function exit: postcondition got status invalid.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:155.
PROJECT_FILE.i:43:[value] Function __gmpz_clear: precondition got status valid.
Called from PROJECT_FILE.i:219.
PROJECT_FILE.i:85:[value] Function __gmpz_clear: precondition got status valid.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:156.
Called from PROJECT_FILE.i:220.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:172.
Called from PROJECT_FILE.i:236.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:173.
Called from PROJECT_FILE.i:237.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:174.
Called from PROJECT_FILE.i:238.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:175.
Called from PROJECT_FILE.i:239.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:176.
Called from PROJECT_FILE.i:240.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:177.
Called from PROJECT_FILE.i:241.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:181.
Called from PROJECT_FILE.i:245.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:182.
Called from PROJECT_FILE.i:246.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:183.
Called from PROJECT_FILE.i:247.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:184.
Called from PROJECT_FILE.i:248.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:185.
Called from PROJECT_FILE.i:249.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:186.
Called from PROJECT_FILE.i:250.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:200.
Called from PROJECT_FILE.i:264.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:201.
Called from PROJECT_FILE.i:265.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:202.
Called from PROJECT_FILE.i:266.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:203.
Called from PROJECT_FILE.i:267.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:204.
Called from PROJECT_FILE.i:268.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:205.
Called from PROJECT_FILE.i:269.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:209.
Called from PROJECT_FILE.i:273.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:210.
Called from PROJECT_FILE.i:274.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:211.
Called from PROJECT_FILE.i:275.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:212.
Called from PROJECT_FILE.i:276.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:213.
Called from PROJECT_FILE.i:277.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:214.
Called from PROJECT_FILE.i:278.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:225.
Called from PROJECT_FILE.i:289.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:226.
Called from PROJECT_FILE.i:290.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:227.
Called from PROJECT_FILE.i:291.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:228.
Called from PROJECT_FILE.i:292.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:229.
Called from PROJECT_FILE.i:293.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:230.
Called from PROJECT_FILE.i:294.
[value] Done for function __gmpz_clear
[value] Recording results for main
[value] done for function main
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
+ 1
− 1
View file @ b2256999
......@@ -2,7 +2,7 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
PROJECT_FILE.i:136:[value] Assertion got status valid.
PROJECT_FILE.i:200:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle
+ 1
− 1
View file @ b2256999
......@@ -2,7 +2,7 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
PROJECT_FILE.i:134:[value] Assertion got status unknown.
PROJECT_FILE.i:198:[value] Assertion got status unknown.
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
+ 14
− 14
View file @ b2256999
......@@ -2,33 +2,33 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
PROJECT_FILE.i:138:[value] Assertion got status unknown.
PROJECT_FILE.i:141:[value] Assertion got status valid.
PROJECT_FILE.i:202:[value] Assertion got status unknown.
PROJECT_FILE.i:205:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:145.
PROJECT_FILE.i:33:[value] Function __gmpz_init_set_si: postcondition got status valid.
Called from PROJECT_FILE.i:209.
PROJECT_FILE.i:75:[value] Function __gmpz_init_set_si: postcondition got status valid.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:146.
PROJECT_FILE.i:49:[value] Function __gmpz_cmp: precondition got status valid.
PROJECT_FILE.i:50:[value] Function __gmpz_cmp: precondition got status valid.
Called from PROJECT_FILE.i:210.
PROJECT_FILE.i:91:[value] Function __gmpz_cmp: precondition got status valid.
PROJECT_FILE.i:92:[value] Function __gmpz_cmp: precondition got status valid.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:147.
Called from PROJECT_FILE.i:211.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
PROJECT_FILE.i:119:[value] Function exit: postcondition got status invalid.
Called from PROJECT_FILE.i:193.
PROJECT_FILE.i:183:[value] Function exit: postcondition got status invalid.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:148.
PROJECT_FILE.i:43:[value] Function __gmpz_clear: precondition got status valid.
Called from PROJECT_FILE.i:212.
PROJECT_FILE.i:85:[value] Function __gmpz_clear: precondition got status valid.
[value] Done for function __gmpz_clear
PROJECT_FILE.i:152:[value] Assertion got status valid.
PROJECT_FILE.i:216:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
+ 33
− 33
View file @ b2256999
......@@ -5,81 +5,81 @@ tests/e-acsl-runtime/result.i:6:[e-acsl] warning: missing guard for ensuring tha
[value] Values of globals at initialization
Y ∈ {1}
[value] computing for function f <- main.
Called from PROJECT_FILE.i:188.
Called from PROJECT_FILE.i:252.
[value] computing for function __gmpz_init_set_si <- f <- main.
Called from PROJECT_FILE.i:143.
PROJECT_FILE.i:33:[value] Function __gmpz_init_set_si: postcondition got status valid.
Called from PROJECT_FILE.i:207.
PROJECT_FILE.i:75:[value] Function __gmpz_init_set_si: postcondition got status valid.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- f <- main.
Called from PROJECT_FILE.i:144.
PROJECT_FILE.i:21:[value] Function __gmpz_init: postcondition got status valid.
Called from PROJECT_FILE.i:208.
PROJECT_FILE.i:63:[value] Function __gmpz_init: postcondition got status valid.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_sub <- f <- main.
Called from PROJECT_FILE.i:145.
PROJECT_FILE.i:70:[value] Function __gmpz_sub: precondition got status valid.
PROJECT_FILE.i:71:[value] Function __gmpz_sub: precondition got status valid.
PROJECT_FILE.i:72:[value] Function __gmpz_sub: precondition got status valid.
Called from PROJECT_FILE.i:209.
PROJECT_FILE.i:112:[value] Function __gmpz_sub: precondition got status valid.
PROJECT_FILE.i:113:[value] Function __gmpz_sub: precondition got status valid.
PROJECT_FILE.i:114:[value] Function __gmpz_sub: precondition got status valid.
[value] Done for function __gmpz_sub
[value] computing for function __gmpz_get_si <- f <- main.
Called from PROJECT_FILE.i:146.
PROJECT_FILE.i:96:[value] Function __gmpz_get_si: precondition got status valid.
Called from PROJECT_FILE.i:210.
PROJECT_FILE.i:138:[value] Function __gmpz_get_si: precondition got status valid.
[value] Done for function __gmpz_get_si
[value] computing for function e_acsl_fail <- f <- main.
Called from PROJECT_FILE.i:148.
Called from PROJECT_FILE.i:212.
[value] computing for function printf <- e_acsl_fail <- f <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- f <- main.
Called from PROJECT_FILE.i:129.
PROJECT_FILE.i:119:[value] Function exit: postcondition got status invalid.
Called from PROJECT_FILE.i:193.
PROJECT_FILE.i:183:[value] Function exit: postcondition got status invalid.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- f <- main.
Called from PROJECT_FILE.i:150.
PROJECT_FILE.i:43:[value] Function __gmpz_clear: precondition got status valid.
Called from PROJECT_FILE.i:214.
PROJECT_FILE.i:85:[value] Function __gmpz_clear: precondition got status valid.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- f <- main.
Called from PROJECT_FILE.i:151.
Called from PROJECT_FILE.i:215.
[value] Done for function __gmpz_clear
PROJECT_FILE.i:131:[value] Function f: postcondition got status valid.
PROJECT_FILE.i:195:[value] Function f: postcondition got status valid.
[value] Recording results for f
[value] Done for function f
[value] computing for function g <- main.
Called from PROJECT_FILE.i:189.
PROJECT_FILE.i:158:[value] Function g: postcondition got status valid.
Called from PROJECT_FILE.i:253.
PROJECT_FILE.i:222:[value] Function g: postcondition got status valid.
[value] Recording results for g
[value] Done for function g
[value] computing for function h <- main.
Called from PROJECT_FILE.i:190.
Called from PROJECT_FILE.i:254.
[value] computing for function __gmpz_init_set_si <- h <- main.
Called from PROJECT_FILE.i:174.
Called from PROJECT_FILE.i:238.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- h <- main.
Called from PROJECT_FILE.i:175.
Called from PROJECT_FILE.i:239.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- h <- main.
Called from PROJECT_FILE.i:176.
PROJECT_FILE.i:49:[value] Function __gmpz_cmp: precondition got status valid.
PROJECT_FILE.i:50:[value] Function __gmpz_cmp: precondition got status valid.
Called from PROJECT_FILE.i:240.
PROJECT_FILE.i:91:[value] Function __gmpz_cmp: precondition got status valid.
PROJECT_FILE.i:92:[value] Function __gmpz_cmp: precondition got status valid.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- h <- main.
Called from PROJECT_FILE.i:177.
Called from PROJECT_FILE.i:241.
[value] computing for function printf <- e_acsl_fail <- h <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- h <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- h <- main.
Called from PROJECT_FILE.i:178.
Called from PROJECT_FILE.i:242.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- h <- main.
Called from PROJECT_FILE.i:179.
Called from PROJECT_FILE.i:243.
[value] Done for function __gmpz_clear
PROJECT_FILE.i:165:[value] Function h: postcondition got status valid.
PROJECT_FILE.i:229:[value] Function h: postcondition got status valid.
[value] Recording results for h
[value] Done for function h
[value] Recording results for main
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
+ 23
− 23
View file @ b2256999
......@@ -2,62 +2,62 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
PROJECT_FILE.i:136:[value] Assertion got status valid.
PROJECT_FILE.i:200:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:141.
PROJECT_FILE.i:33:[value] Function __gmpz_init_set_si: postcondition got status valid.
Called from PROJECT_FILE.i:205.
PROJECT_FILE.i:75:[value] Function __gmpz_init_set_si: postcondition got status valid.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:142.
Called from PROJECT_FILE.i:206.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:143.
PROJECT_FILE.i:49:[value] Function __gmpz_cmp: precondition got status valid.
PROJECT_FILE.i:50:[value] Function __gmpz_cmp: precondition got status valid.
Called from PROJECT_FILE.i:207.
PROJECT_FILE.i:91:[value] Function __gmpz_cmp: precondition got status valid.
PROJECT_FILE.i:92:[value] Function __gmpz_cmp: precondition got status valid.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:144.
Called from PROJECT_FILE.i:208.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
PROJECT_FILE.i:119:[value] Function exit: postcondition got status invalid.
Called from PROJECT_FILE.i:193.
PROJECT_FILE.i:183:[value] Function exit: postcondition got status invalid.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:145.
PROJECT_FILE.i:43:[value] Function __gmpz_clear: precondition got status valid.
Called from PROJECT_FILE.i:209.
PROJECT_FILE.i:85:[value] Function __gmpz_clear: precondition got status valid.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:146.
Called from PROJECT_FILE.i:210.
[value] Done for function __gmpz_clear
PROJECT_FILE.i:150:[value] Assertion got status valid.
PROJECT_FILE.i:214:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:155.
Called from PROJECT_FILE.i:219.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
Called from PROJECT_FILE.i:156.
Called from PROJECT_FILE.i:220.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
Called from PROJECT_FILE.i:157.
Called from PROJECT_FILE.i:221.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:159.
Called from PROJECT_FILE.i:223.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
Called from PROJECT_FILE.i:193.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:161.
Called from PROJECT_FILE.i:225.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
Called from PROJECT_FILE.i:162.
Called from PROJECT_FILE.i:226.
[value] Done for function __gmpz_clear
[value] Recording results for main
[value] done for function main
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
+ 1
− 1
View file @ b2256999
......@@ -2,7 +2,7 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
PROJECT_FILE.i:136:[value] Assertion got status valid.
PROJECT_FILE.i:200:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment