From b22569994cfea360042896b0411b4e830545edc1 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 8 Dec 2011 08:41:23 +0000
Subject: [PATCH] updating tests for farm-lsl-cloud
---
.../e-acsl-runtime/oracle/addrOf.res.oracle | 2 +-
.../e-acsl-runtime/oracle/arith.res.oracle | 584 +++++++++---------
.../e-acsl-runtime/oracle/array.res.oracle | 24 +-
.../tests/e-acsl-runtime/oracle/at.res.oracle | 242 ++++----
.../e-acsl-runtime/oracle/cast.res.oracle | 38 +-
.../oracle/comparison.res.oracle | 212 +++----
.../oracle/function_contract.res.oracle | 374 +++++------
.../oracle/integer_constant.res.oracle | 28 +-
.../e-acsl-runtime/oracle/lazy.res.oracle | 144 ++---
.../oracle/nested_code_annot.res.oracle | 108 ++--
.../e-acsl-runtime/oracle/not.res.oracle | 2 +-
.../e-acsl-runtime/oracle/null.res.oracle | 2 +-
.../oracle/other_constants.res.oracle | 28 +-
.../e-acsl-runtime/oracle/ptr.res.oracle | 370 +++++------
.../e-acsl-runtime/oracle/result.res.oracle | 66 +-
.../e-acsl-runtime/oracle/sizeof.res.oracle | 46 +-
.../oracle/stmt_contract.res.oracle | 360 +++++------
.../e-acsl-runtime/oracle/true.res.oracle | 2 +-
18 files changed, 1316 insertions(+), 1316 deletions(-)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
index d76d6369f19..c9325f8777a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
@@ -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 ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
index 667ac7338dc..496ec7bebca 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
@@ -3,808 +3,808 @@
[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 <- main.
- Called from PROJECT_FILE.i:145.
-PROJECT_FILE.i:21:[value] Function __gmpz_init: postcondition got status valid.
+ Called from PROJECT_FILE.i:209.
+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:146.
-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:210.
+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:147.
+ Called from PROJECT_FILE.i:211.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:148.
-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:212.
+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: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 <- main.
- Called from PROJECT_FILE.i:151.
+ Called from PROJECT_FILE.i:215.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:152.
+ Called from PROJECT_FILE.i:216.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:156:[value] Assertion got status valid.
+PROJECT_FILE.i:220:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:162.
+ Called from PROJECT_FILE.i:226.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:163.
+ Called from PROJECT_FILE.i:227.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:164.
+ Called from PROJECT_FILE.i:228.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_neg <- main.
- Called from PROJECT_FILE.i:165.
+ Called from PROJECT_FILE.i:229.
[value] Done for function __gmpz_neg
[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
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:170.
+ Called from PROJECT_FILE.i:234.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:174:[value] Assertion got status valid.
+PROJECT_FILE.i:238:[value] Assertion got status valid.
[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
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:180.
+ Called from PROJECT_FILE.i:244.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_com <- main.
- Called from PROJECT_FILE.i:181.
+ Called from PROJECT_FILE.i:245.
[kernel] warning: No code for function __gmpz_com, default assigns generated
[value] Done for function __gmpz_com
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:182.
+ Called from PROJECT_FILE.i:246.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:183.
+ Called from PROJECT_FILE.i:247.
[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:184.
+ Called from PROJECT_FILE.i:248.
[value] Done for function __gmpz_clear
[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
-PROJECT_FILE.i:189:[value] Assertion got status valid.
+PROJECT_FILE.i:253:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:197.
+ Called from PROJECT_FILE.i:261.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:198.
+ Called from PROJECT_FILE.i:262.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:199.
+ Called from PROJECT_FILE.i:263.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_add <- main.
- Called from PROJECT_FILE.i:200.
-PROJECT_FILE.i:64:[value] Function __gmpz_add: precondition got status valid.
-PROJECT_FILE.i:65:[value] Function __gmpz_add: precondition got status valid.
-PROJECT_FILE.i:66:[value] Function __gmpz_add: precondition got status valid.
+ Called from PROJECT_FILE.i:264.
+PROJECT_FILE.i:106:[value] Function __gmpz_add: precondition got status valid.
+PROJECT_FILE.i:107:[value] Function __gmpz_add: precondition got status valid.
+PROJECT_FILE.i:108:[value] Function __gmpz_add: precondition got status valid.
[value] Done for function __gmpz_add
[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_init <- main.
- Called from PROJECT_FILE.i:202.
+ Called from PROJECT_FILE.i:266.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_neg <- main.
- Called from PROJECT_FILE.i:203.
+ Called from PROJECT_FILE.i:267.
[value] Done for function __gmpz_neg
[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 e_acsl_fail <- main.
- Called from PROJECT_FILE.i:205.
+ Called from PROJECT_FILE.i:269.
[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:206.
+ Called from PROJECT_FILE.i:270.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:207.
+ Called from PROJECT_FILE.i:271.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:208.
+ Called from PROJECT_FILE.i:272.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:209.
+ Called from PROJECT_FILE.i:273.
[value] Done for function __gmpz_clear
[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
-PROJECT_FILE.i:214:[value] Assertion got status valid.
+PROJECT_FILE.i:278:[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_sub <- main.
- Called from PROJECT_FILE.i:225.
-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:289.
+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_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_init <- main.
- Called from PROJECT_FILE.i:227.
+ Called from PROJECT_FILE.i:291.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_neg <- main.
- Called from PROJECT_FILE.i:228.
+ Called from PROJECT_FILE.i:292.
[value] Done for function __gmpz_neg
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:229.
+ Called from PROJECT_FILE.i:293.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:230.
+ Called from PROJECT_FILE.i:294.
[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:231.
+ Called from PROJECT_FILE.i:295.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:232.
+ Called from PROJECT_FILE.i:296.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:233.
+ Called from PROJECT_FILE.i:297.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:234.
+ Called from PROJECT_FILE.i:298.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:235.
+ Called from PROJECT_FILE.i:299.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:239:[value] Assertion got status valid.
+PROJECT_FILE.i:303:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:247.
+ Called from PROJECT_FILE.i:311.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:248.
+ Called from PROJECT_FILE.i:312.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:249.
+ Called from PROJECT_FILE.i:313.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_mul <- main.
- Called from PROJECT_FILE.i:250.
-PROJECT_FILE.i:76:[value] Function __gmpz_mul: precondition got status valid.
-PROJECT_FILE.i:77:[value] Function __gmpz_mul: precondition got status valid.
-PROJECT_FILE.i:78:[value] Function __gmpz_mul: precondition got status valid.
+ Called from PROJECT_FILE.i:314.
+PROJECT_FILE.i:118:[value] Function __gmpz_mul: precondition got status valid.
+PROJECT_FILE.i:119:[value] Function __gmpz_mul: precondition got status valid.
+PROJECT_FILE.i:120:[value] Function __gmpz_mul: precondition got status valid.
[value] Done for function __gmpz_mul
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:251.
+ Called from PROJECT_FILE.i:315.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:252.
+ Called from PROJECT_FILE.i:316.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_neg <- main.
- Called from PROJECT_FILE.i:253.
+ Called from PROJECT_FILE.i:317.
[value] Done for function __gmpz_neg
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:254.
+ Called from PROJECT_FILE.i:318.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:255.
+ Called from PROJECT_FILE.i:319.
[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:256.
+ Called from PROJECT_FILE.i:320.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:257.
+ Called from PROJECT_FILE.i:321.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:258.
+ Called from PROJECT_FILE.i:322.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:259.
+ Called from PROJECT_FILE.i:323.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:260.
+ Called from PROJECT_FILE.i:324.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:264:[value] Assertion got status valid.
+PROJECT_FILE.i:328:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:273.
+ Called from PROJECT_FILE.i:337.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:274.
+ Called from PROJECT_FILE.i:338.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_get_si <- main.
- Called from PROJECT_FILE.i:275.
-PROJECT_FILE.i:96:[value] Function __gmpz_get_si: precondition got status valid.
+ Called from PROJECT_FILE.i:339.
+PROJECT_FILE.i:138:[value] Function __gmpz_get_si: precondition got status valid.
[value] Done for function __gmpz_get_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
-PROJECT_FILE.i:277:[value] Assertion got status valid.
+PROJECT_FILE.i:341:[value] Assertion got status valid.
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:278.
+ Called from PROJECT_FILE.i:342.
[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_tdiv_q <- main.
- Called from PROJECT_FILE.i:279.
-PROJECT_FILE.i:82:[value] Function __gmpz_tdiv_q: precondition got status valid.
-PROJECT_FILE.i:83:[value] Function __gmpz_tdiv_q: precondition got status valid.
-PROJECT_FILE.i:84:[value] Function __gmpz_tdiv_q: precondition got status valid.
+ Called from PROJECT_FILE.i:343.
+PROJECT_FILE.i:124:[value] Function __gmpz_tdiv_q: precondition got status valid.
+PROJECT_FILE.i:125:[value] Function __gmpz_tdiv_q: precondition got status valid.
+PROJECT_FILE.i:126:[value] Function __gmpz_tdiv_q: precondition got status valid.
[value] Done for function __gmpz_tdiv_q
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:280.
+ Called from PROJECT_FILE.i:344.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:281.
+ Called from PROJECT_FILE.i:345.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_neg <- main.
- Called from PROJECT_FILE.i:282.
+ Called from PROJECT_FILE.i:346.
[value] Done for function __gmpz_neg
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:283.
+ Called from PROJECT_FILE.i:347.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:284.
+ Called from PROJECT_FILE.i:348.
[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:285.
+ Called from PROJECT_FILE.i:349.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:286.
+ Called from PROJECT_FILE.i:350.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:287.
+ Called from PROJECT_FILE.i:351.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:288.
+ Called from PROJECT_FILE.i:352.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:289.
+ Called from PROJECT_FILE.i:353.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:293:[value] Assertion got status valid.
+PROJECT_FILE.i:357:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_str <- main.
- Called from PROJECT_FILE.i:301.
-PROJECT_FILE.i:37:[value] Function __gmpz_init_set_str: postcondition got status valid.
+ Called from PROJECT_FILE.i:365.
+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_init_set_si <- main.
- Called from PROJECT_FILE.i:302.
+ Called from PROJECT_FILE.i:366.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:303.
+ Called from PROJECT_FILE.i:367.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:304.
+ Called from PROJECT_FILE.i:368.
[value] Done for function __gmpz_init
-PROJECT_FILE.i:305:[value] Assertion got status valid.
+PROJECT_FILE.i:369:[value] Assertion got status valid.
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:306.
+ Called from PROJECT_FILE.i:370.
[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_tdiv_q <- main.
- Called from PROJECT_FILE.i:307.
+ Called from PROJECT_FILE.i:371.
[value] Done for function __gmpz_tdiv_q
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:308.
+ Called from PROJECT_FILE.i:372.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:309.
+ Called from PROJECT_FILE.i:373.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:311.
+ Called from PROJECT_FILE.i:375.
[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:313.
+ Called from PROJECT_FILE.i:377.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:314.
+ Called from PROJECT_FILE.i:378.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:315.
+ Called from PROJECT_FILE.i:379.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:316.
+ Called from PROJECT_FILE.i:380.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:320:[value] Assertion got status valid.
+PROJECT_FILE.i:384:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:329.
+ Called from PROJECT_FILE.i:393.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:330.
+ Called from PROJECT_FILE.i:394.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_get_si <- main.
- Called from PROJECT_FILE.i:331.
+ Called from PROJECT_FILE.i:395.
[value] Done for function __gmpz_get_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:332.
+ Called from PROJECT_FILE.i:396.
[value] Done for function __gmpz_init
-PROJECT_FILE.i:333:[value] Assertion got status valid.
+PROJECT_FILE.i:397:[value] Assertion got status valid.
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:334.
+ Called from PROJECT_FILE.i:398.
[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_tdiv_r <- main.
- Called from PROJECT_FILE.i:335.
-PROJECT_FILE.i:88:[value] Function __gmpz_tdiv_r: precondition got status valid.
-PROJECT_FILE.i:89:[value] Function __gmpz_tdiv_r: precondition got status valid.
-PROJECT_FILE.i:90:[value] Function __gmpz_tdiv_r: precondition got status valid.
+ Called from PROJECT_FILE.i:399.
+PROJECT_FILE.i:130:[value] Function __gmpz_tdiv_r: precondition got status valid.
+PROJECT_FILE.i:131:[value] Function __gmpz_tdiv_r: precondition got status valid.
+PROJECT_FILE.i:132:[value] Function __gmpz_tdiv_r: precondition got status valid.
[value] Done for function __gmpz_tdiv_r
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:336.
+ Called from PROJECT_FILE.i:400.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:337.
+ Called from PROJECT_FILE.i:401.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_neg <- main.
- Called from PROJECT_FILE.i:338.
+ Called from PROJECT_FILE.i:402.
[value] Done for function __gmpz_neg
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:339.
+ Called from PROJECT_FILE.i:403.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:340.
+ Called from PROJECT_FILE.i:404.
[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:341.
+ Called from PROJECT_FILE.i:405.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:342.
+ Called from PROJECT_FILE.i:406.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:343.
+ Called from PROJECT_FILE.i:407.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:344.
+ Called from PROJECT_FILE.i:408.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:345.
+ Called from PROJECT_FILE.i:409.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:349:[value] Assertion got status valid.
+PROJECT_FILE.i:413:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:361.
+ Called from PROJECT_FILE.i:425.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:362.
+ Called from PROJECT_FILE.i:426.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_neg <- main.
- Called from PROJECT_FILE.i:363.
+ Called from PROJECT_FILE.i:427.
[value] Done for function __gmpz_neg
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:364.
+ Called from PROJECT_FILE.i:428.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:365.
+ Called from PROJECT_FILE.i:429.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_neg <- main.
- Called from PROJECT_FILE.i:366.
+ Called from PROJECT_FILE.i:430.
[value] Done for function __gmpz_neg
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:367.
+ Called from PROJECT_FILE.i:431.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:368.
+ Called from PROJECT_FILE.i:432.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:369.
+ Called from PROJECT_FILE.i:433.
[value] Done for function __gmpz_init
-PROJECT_FILE.i:370:[value] Assertion got status valid.
+PROJECT_FILE.i:434:[value] Assertion got status valid.
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:371.
+ Called from PROJECT_FILE.i:435.
[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_tdiv_r <- main.
- Called from PROJECT_FILE.i:372.
+ Called from PROJECT_FILE.i:436.
[value] Done for function __gmpz_tdiv_r
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:373.
+ Called from PROJECT_FILE.i:437.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:374.
+ Called from PROJECT_FILE.i:438.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_neg <- main.
- Called from PROJECT_FILE.i:375.
+ Called from PROJECT_FILE.i:439.
[value] Done for function __gmpz_neg
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:376.
+ Called from PROJECT_FILE.i:440.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:377.
+ Called from PROJECT_FILE.i:441.
[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:378.
+ Called from PROJECT_FILE.i:442.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:379.
+ Called from PROJECT_FILE.i:443.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:380.
+ Called from PROJECT_FILE.i:444.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:381.
+ Called from PROJECT_FILE.i:445.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:382.
+ Called from PROJECT_FILE.i:446.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:383.
+ Called from PROJECT_FILE.i:447.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:384.
+ Called from PROJECT_FILE.i:448.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:385.
+ Called from PROJECT_FILE.i:449.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:389:[value] Assertion got status valid.
+PROJECT_FILE.i:453:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:399.
+ Called from PROJECT_FILE.i:463.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:400.
+ Called from PROJECT_FILE.i:464.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:401.
+ Called from PROJECT_FILE.i:465.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_neg <- main.
- Called from PROJECT_FILE.i:402.
+ Called from PROJECT_FILE.i:466.
[value] Done for function __gmpz_neg
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:403.
+ Called from PROJECT_FILE.i:467.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:404.
+ Called from PROJECT_FILE.i:468.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:405.
+ Called from PROJECT_FILE.i:469.
[value] Done for function __gmpz_init
-PROJECT_FILE.i:406:[value] Assertion got status valid.
+PROJECT_FILE.i:470:[value] Assertion got status valid.
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:407.
+ Called from PROJECT_FILE.i:471.
[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_tdiv_r <- main.
- Called from PROJECT_FILE.i:408.
+ Called from PROJECT_FILE.i:472.
[value] Done for function __gmpz_tdiv_r
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:409.
+ Called from PROJECT_FILE.i:473.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:410.
+ Called from PROJECT_FILE.i:474.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:411.
+ Called from PROJECT_FILE.i:475.
[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:412.
+ Called from PROJECT_FILE.i:476.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:413.
+ Called from PROJECT_FILE.i:477.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:414.
+ Called from PROJECT_FILE.i:478.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:415.
+ Called from PROJECT_FILE.i:479.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:416.
+ Called from PROJECT_FILE.i:480.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:417.
+ Called from PROJECT_FILE.i:481.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:421:[value] Assertion got status valid.
+PROJECT_FILE.i:485:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:437.
+ Called from PROJECT_FILE.i:501.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:438.
+ Called from PROJECT_FILE.i:502.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:439.
+ Called from PROJECT_FILE.i:503.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_mul <- main.
- Called from PROJECT_FILE.i:440.
+ Called from PROJECT_FILE.i:504.
[value] Done for function __gmpz_mul
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:441.
+ Called from PROJECT_FILE.i:505.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:442.
+ Called from PROJECT_FILE.i:506.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:443.
+ Called from PROJECT_FILE.i:507.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_add <- main.
- Called from PROJECT_FILE.i:444.
+ Called from PROJECT_FILE.i:508.
[value] Done for function __gmpz_add
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:445.
+ Called from PROJECT_FILE.i:509.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_add <- main.
- Called from PROJECT_FILE.i:446.
+ Called from PROJECT_FILE.i:510.
[value] Done for function __gmpz_add
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:447.
+ Called from PROJECT_FILE.i:511.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:448.
+ Called from PROJECT_FILE.i:512.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_sub <- main.
- Called from PROJECT_FILE.i:449.
+ Called from PROJECT_FILE.i:513.
[value] Done for function __gmpz_sub
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:450.
+ Called from PROJECT_FILE.i:514.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_sub <- main.
- Called from PROJECT_FILE.i:451.
+ Called from PROJECT_FILE.i:515.
[value] Done for function __gmpz_sub
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:452.
+ Called from PROJECT_FILE.i:516.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_add <- main.
- Called from PROJECT_FILE.i:453.
+ Called from PROJECT_FILE.i:517.
[value] Done for function __gmpz_add
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:454.
+ Called from PROJECT_FILE.i:518.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:455.
+ Called from PROJECT_FILE.i:519.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_neg <- main.
- Called from PROJECT_FILE.i:456.
+ Called from PROJECT_FILE.i:520.
[value] Done for function __gmpz_neg
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:457.
+ Called from PROJECT_FILE.i:521.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:458.
+ Called from PROJECT_FILE.i:522.
[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:460.
+ Called from PROJECT_FILE.i:524.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:461.
+ Called from PROJECT_FILE.i:525.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:462.
+ Called from PROJECT_FILE.i:526.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:463.
+ Called from PROJECT_FILE.i:527.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:464.
+ Called from PROJECT_FILE.i:528.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:465.
+ Called from PROJECT_FILE.i:529.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:466.
+ Called from PROJECT_FILE.i:530.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:467.
+ Called from PROJECT_FILE.i:531.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:468.
+ Called from PROJECT_FILE.i:532.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:469.
+ Called from PROJECT_FILE.i:533.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:470.
+ Called from PROJECT_FILE.i:534.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:471.
+ Called from PROJECT_FILE.i:535.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:472.
+ Called from PROJECT_FILE.i:536.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:476:[value] Assertion got status valid.
-PROJECT_FILE.i:479:[value] Assertion got status valid.
+PROJECT_FILE.i:540:[value] Assertion got status valid.
+PROJECT_FILE.i:543:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:485.
+ Called from PROJECT_FILE.i:549.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:486.
+ Called from PROJECT_FILE.i:550.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:487.
+ Called from PROJECT_FILE.i:551.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_neg <- main.
- Called from PROJECT_FILE.i:488.
+ Called from PROJECT_FILE.i:552.
[value] Done for function __gmpz_neg
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:489.
+ Called from PROJECT_FILE.i:553.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:490.
+ Called from PROJECT_FILE.i:554.
[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:492.
+ Called from PROJECT_FILE.i:556.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:493.
+ Called from PROJECT_FILE.i:557.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:494.
+ Called from PROJECT_FILE.i:558.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:498:[value] Assertion got status valid.
+PROJECT_FILE.i:562:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:504.
+ Called from PROJECT_FILE.i:568.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:505.
+ Called from PROJECT_FILE.i:569.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:506.
+ Called from PROJECT_FILE.i:570.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_neg <- main.
- Called from PROJECT_FILE.i:507.
+ Called from PROJECT_FILE.i:571.
[value] Done for function __gmpz_neg
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:508.
+ Called from PROJECT_FILE.i:572.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:510.
+ Called from PROJECT_FILE.i:574.
[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:512.
+ Called from PROJECT_FILE.i:576.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:513.
+ Called from PROJECT_FILE.i:577.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:514.
+ Called from PROJECT_FILE.i:578.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:518:[value] Assertion got status valid.
-PROJECT_FILE.i:521:[value] Assertion got status valid.
+PROJECT_FILE.i:582:[value] Assertion got status valid.
+PROJECT_FILE.i:585:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
index 60f253ae3c0..e66926fef9f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
@@ -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
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
index 84ff0279486..9a11dfeb733 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
@@ -10,338 +10,338 @@ tests/e-acsl-runtime/at.i:33:[e-acsl] warning: missing guard for ensuring that p
[value] Values of globals at initialization
A ∈ {0}
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:291.
-PROJECT_FILE.i:33:[value] Function __gmpz_init_set_si: postcondition got status valid.
+ Called from PROJECT_FILE.i:355.
+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: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.
-PROJECT_FILE.i:21:[value] Function __gmpz_init: postcondition got status valid.
+ Called from PROJECT_FILE.i:357.
+PROJECT_FILE.i:63:[value] Function __gmpz_init: postcondition got status valid.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_add <- main.
- Called from PROJECT_FILE.i:294.
-PROJECT_FILE.i:64:[value] Function __gmpz_add: precondition got status valid.
-PROJECT_FILE.i:65:[value] Function __gmpz_add: precondition got status valid.
-PROJECT_FILE.i:66:[value] Function __gmpz_add: precondition got status valid.
+ Called from PROJECT_FILE.i:358.
+PROJECT_FILE.i:106:[value] Function __gmpz_add: precondition got status valid.
+PROJECT_FILE.i:107:[value] Function __gmpz_add: precondition got status valid.
+PROJECT_FILE.i:108:[value] Function __gmpz_add: precondition got status valid.
[value] Done for function __gmpz_add
[value] computing for function __gmpz_init_set <- main.
- Called from PROJECT_FILE.i:295.
-PROJECT_FILE.i:25:[value] Function __gmpz_init_set: postcondition got status valid.
+ Called from PROJECT_FILE.i:359.
+PROJECT_FILE.i:67:[value] Function __gmpz_init_set: postcondition got status valid.
[value] Done for function __gmpz_init_set
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:296.
-PROJECT_FILE.i:43:[value] Function __gmpz_clear: precondition got status valid.
+ Called from PROJECT_FILE.i:360.
+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: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
-PROJECT_FILE.i:302:[value] Assertion got status valid.
+PROJECT_FILE.i:366:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:307.
+ Called from PROJECT_FILE.i:371.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:308.
+ Called from PROJECT_FILE.i:372.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:309.
-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:373.
+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:310.
+ Called from PROJECT_FILE.i:374.
[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:311.
+ Called from PROJECT_FILE.i:375.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:312.
+ Called from PROJECT_FILE.i:376.
[value] Done for function __gmpz_clear
[value] computing for function f <- main.
- Called from PROJECT_FILE.i:318.
-PROJECT_FILE.i:148:[value] Assertion got status valid.
+ Called from PROJECT_FILE.i:382.
+PROJECT_FILE.i:212:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- f <- main.
- Called from PROJECT_FILE.i:153.
+ Called from PROJECT_FILE.i:217.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- f <- main.
- Called from PROJECT_FILE.i:154.
+ Called from PROJECT_FILE.i:218.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- f <- main.
- Called from PROJECT_FILE.i:155.
+ Called from PROJECT_FILE.i:219.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- f <- main.
- Called from PROJECT_FILE.i:156.
+ Called from PROJECT_FILE.i:220.
[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.
+ 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 <- f <- main.
- Called from PROJECT_FILE.i:157.
+ Called from PROJECT_FILE.i:221.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- f <- main.
- Called from PROJECT_FILE.i:158.
+ Called from PROJECT_FILE.i:222.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:162:[value] Assertion got status unknown.
+PROJECT_FILE.i:226:[value] Assertion got status unknown.
[value] computing for function __gmpz_init_set_si <- f <- main.
- Called from PROJECT_FILE.i:167.
+ Called from PROJECT_FILE.i:231.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- f <- main.
- Called from PROJECT_FILE.i:168.
+ Called from PROJECT_FILE.i:232.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- f <- main.
- Called from PROJECT_FILE.i:169.
+ Called from PROJECT_FILE.i:233.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- f <- main.
- Called from PROJECT_FILE.i:170.
+ Called from PROJECT_FILE.i:234.
[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.
+ 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 <- f <- main.
- Called from PROJECT_FILE.i:171.
+ Called from PROJECT_FILE.i:235.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- f <- main.
- Called from PROJECT_FILE.i:172.
+ Called from PROJECT_FILE.i:236.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:176:[value] Assertion got status valid.
+PROJECT_FILE.i:240:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- f <- 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_init_set_si <- f <- main.
- Called from PROJECT_FILE.i:183.
+ Called from PROJECT_FILE.i:247.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- f <- main.
- Called from PROJECT_FILE.i:184.
+ Called from PROJECT_FILE.i:248.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- f <- main.
- Called from PROJECT_FILE.i:185.
+ Called from PROJECT_FILE.i:249.
[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.
+ 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 <- f <- main.
- Called from PROJECT_FILE.i:186.
+ Called from PROJECT_FILE.i:250.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- f <- main.
- Called from PROJECT_FILE.i:187.
+ Called from PROJECT_FILE.i:251.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:191:[value] Assertion got status unknown.
+PROJECT_FILE.i:255:[value] Assertion got status unknown.
[value] computing for function __gmpz_init_set_si <- f <- main.
- Called from PROJECT_FILE.i:196.
+ Called from PROJECT_FILE.i:260.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- f <- main.
- Called from PROJECT_FILE.i:197.
+ Called from PROJECT_FILE.i:261.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- f <- main.
- Called from PROJECT_FILE.i:198.
+ Called from PROJECT_FILE.i:262.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- f <- main.
- Called from PROJECT_FILE.i:199.
+ Called from PROJECT_FILE.i:263.
[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.
+ 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 <- f <- main.
- Called from PROJECT_FILE.i:200.
+ Called from PROJECT_FILE.i:264.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- f <- main.
- Called from PROJECT_FILE.i:201.
+ Called from PROJECT_FILE.i:265.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_init_set_si <- f <- 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_init_set_si <- f <- main.
- Called from PROJECT_FILE.i:212.
+ Called from PROJECT_FILE.i:276.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- f <- main.
- Called from PROJECT_FILE.i:213.
+ Called from PROJECT_FILE.i:277.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- f <- main.
- Called from PROJECT_FILE.i:214.
+ Called from PROJECT_FILE.i:278.
[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.
+ 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 <- f <- main.
- Called from PROJECT_FILE.i:215.
+ Called from PROJECT_FILE.i:279.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- f <- main.
- Called from PROJECT_FILE.i:216.
+ Called from PROJECT_FILE.i:280.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:132:[value] Function f: postcondition got status valid.
+PROJECT_FILE.i:196:[value] Function f: postcondition got status valid.
[value] Recording results for f
[value] Done for function f
-PROJECT_FILE.i:319:[value] Assertion got status unknown.
+PROJECT_FILE.i:383:[value] Assertion got status unknown.
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:324.
+ Called from PROJECT_FILE.i:388.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:325.
+ Called from PROJECT_FILE.i:389.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:326.
+ Called from PROJECT_FILE.i:390.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:327.
+ Called from PROJECT_FILE.i:391.
[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:328.
+ Called from PROJECT_FILE.i:392.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:329.
+ Called from PROJECT_FILE.i:393.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:333:[value] Assertion got status unknown.
+PROJECT_FILE.i:397:[value] Assertion got status unknown.
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:337.
+ Called from PROJECT_FILE.i:401.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:338.
+ Called from PROJECT_FILE.i:402.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:339.
+ Called from PROJECT_FILE.i:403.
[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:340.
+ Called from PROJECT_FILE.i:404.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:344:[value] Assertion got status unknown.
+PROJECT_FILE.i:408:[value] Assertion got status unknown.
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:350.
+ Called from PROJECT_FILE.i:414.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:351.
+ Called from PROJECT_FILE.i:415.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:352.
+ Called from PROJECT_FILE.i:416.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_add <- main.
- Called from PROJECT_FILE.i:353.
+ Called from PROJECT_FILE.i:417.
[value] Done for function __gmpz_add
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:354.
+ Called from PROJECT_FILE.i:418.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:355.
+ Called from PROJECT_FILE.i:419.
[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:356.
+ Called from PROJECT_FILE.i:420.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:357.
+ Called from PROJECT_FILE.i:421.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:358.
+ Called from PROJECT_FILE.i:422.
[value] Done for function __gmpz_clear
[value] computing for function g <- main.
- Called from PROJECT_FILE.i:362.
-PROJECT_FILE.i:240:[value] Assertion got status unknown.
+ Called from PROJECT_FILE.i:426.
+PROJECT_FILE.i:304:[value] Assertion got status unknown.
[value] computing for function __gmpz_init_set_si <- g <- main.
- Called from PROJECT_FILE.i:245.
+ Called from PROJECT_FILE.i:309.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- g <- main.
- Called from PROJECT_FILE.i:246.
+ Called from PROJECT_FILE.i:310.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- g <- main.
- Called from PROJECT_FILE.i:247.
+ Called from PROJECT_FILE.i:311.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- g <- main.
- Called from PROJECT_FILE.i:248.
+ Called from PROJECT_FILE.i:312.
[value] computing for function printf <- e_acsl_fail <- g <- 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 <- g <- 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 <- g <- main.
- Called from PROJECT_FILE.i:250.
+ Called from PROJECT_FILE.i:314.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- g <- main.
- Called from PROJECT_FILE.i:251.
+ Called from PROJECT_FILE.i:315.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:256:[value] Assertion got status unknown.
+PROJECT_FILE.i:320:[value] Assertion got status unknown.
[value] computing for function __gmpz_init_set_si <- g <- main.
- Called from PROJECT_FILE.i:262.
+ Called from PROJECT_FILE.i:326.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- g <- main.
- Called from PROJECT_FILE.i:263.
+ Called from PROJECT_FILE.i:327.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- g <- main.
- Called from PROJECT_FILE.i:264.
+ Called from PROJECT_FILE.i:328.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- g <- main.
- Called from PROJECT_FILE.i:266.
+ Called from PROJECT_FILE.i:330.
[value] computing for function printf <- e_acsl_fail <- g <- 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 <- g <- 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 <- g <- main.
- Called from PROJECT_FILE.i:268.
+ Called from PROJECT_FILE.i:332.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- g <- main.
- Called from PROJECT_FILE.i:269.
+ Called from PROJECT_FILE.i:333.
[value] Done for function __gmpz_clear
[value] Recording results for g
[value] Done for function g
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:364.
+ Called from PROJECT_FILE.i:428.
[value] Done for function __gmpz_clear
[value] Recording results for main
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
index 419b294f379..5fcbe123afc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
@@ -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
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
index d5ae506c57d..71c0bf36907 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
@@ -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
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
index 28f4cda1b75..9a1de3a6a92 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
@@ -5,535 +5,535 @@
X ∈ {0}
Y ∈ {2}
[value] computing for function f <- main.
- Called from PROJECT_FILE.i:445.
+ Called from PROJECT_FILE.i:509.
[value] computing for function __gmpz_init_set_si <- f <- 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 <- f <- 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 <- f <- 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 <- f <- main.
- Called from PROJECT_FILE.i:144.
+ Called from PROJECT_FILE.i:208.
[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: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 <- f <- main.
- Called from PROJECT_FILE.i:146.
+ Called from PROJECT_FILE.i:210.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:133:[value] Function f: postcondition got status valid.
+PROJECT_FILE.i:197:[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:446.
+ Called from PROJECT_FILE.i:510.
[value] computing for function __gmpz_init_set_si <- g <- main.
- Called from PROJECT_FILE.i:163.
+ Called from PROJECT_FILE.i:227.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- g <- 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_cmp <- g <- main.
- Called from PROJECT_FILE.i:165.
+ Called from PROJECT_FILE.i:229.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- g <- main.
- Called from PROJECT_FILE.i:166.
+ Called from PROJECT_FILE.i:230.
[value] computing for function printf <- e_acsl_fail <- g <- 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 <- g <- 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_init_set_si <- g <- main.
- Called from PROJECT_FILE.i:167.
+ Called from PROJECT_FILE.i:231.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- g <- main.
- Called from PROJECT_FILE.i:168.
+ Called from PROJECT_FILE.i:232.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- g <- main.
- Called from PROJECT_FILE.i:169.
+ Called from PROJECT_FILE.i:233.
[value] computing for function printf <- e_acsl_fail <- g <- 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 <- g <- 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 <- g <- main.
- Called from PROJECT_FILE.i:170.
+ Called from PROJECT_FILE.i:234.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- g <- main.
- Called from PROJECT_FILE.i:171.
+ Called from PROJECT_FILE.i:235.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- g <- main.
- Called from PROJECT_FILE.i:172.
+ Called from PROJECT_FILE.i:236.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:152:[value] Function g: postcondition got status valid.
-PROJECT_FILE.i:153:[value] Function g: postcondition got status valid.
+PROJECT_FILE.i:216:[value] Function g: postcondition got status valid.
+PROJECT_FILE.i:217:[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:447.
-PROJECT_FILE.i:178:[value] Function h: precondition got status valid.
+ Called from PROJECT_FILE.i:511.
+PROJECT_FILE.i:242:[value] Function h: precondition got status valid.
[value] computing for function __gmpz_init_set_si <- h <- main.
- Called from PROJECT_FILE.i:185.
+ Called from PROJECT_FILE.i:249.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- h <- main.
- Called from PROJECT_FILE.i:186.
+ Called from PROJECT_FILE.i:250.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- h <- main.
- Called from PROJECT_FILE.i:187.
+ Called from PROJECT_FILE.i:251.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- h <- main.
- Called from PROJECT_FILE.i:188.
+ Called from PROJECT_FILE.i:252.
[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:189.
+ Called from PROJECT_FILE.i:253.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- h <- main.
- Called from PROJECT_FILE.i:190.
+ Called from PROJECT_FILE.i:254.
[value] Done for function __gmpz_clear
[value] Recording results for h
[value] Done for function h
[value] computing for function i <- main.
- Called from PROJECT_FILE.i:448.
-PROJECT_FILE.i:197:[value] Function i: precondition got status valid.
-PROJECT_FILE.i:198:[value] Function i: precondition got status valid.
+ Called from PROJECT_FILE.i:512.
+PROJECT_FILE.i:261:[value] Function i: precondition got status valid.
+PROJECT_FILE.i:262:[value] Function i: precondition got status valid.
[value] computing for function __gmpz_init_set_si <- i <- main.
- Called from PROJECT_FILE.i:208.
+ Called from PROJECT_FILE.i:272.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- i <- 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_cmp <- i <- main.
- Called from PROJECT_FILE.i:210.
+ Called from PROJECT_FILE.i:274.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- i <- main.
- Called from PROJECT_FILE.i:211.
+ Called from PROJECT_FILE.i:275.
[value] computing for function printf <- e_acsl_fail <- i <- 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 <- i <- 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_init_set_si <- i <- main.
- Called from PROJECT_FILE.i:212.
+ Called from PROJECT_FILE.i:276.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- i <- main.
- Called from PROJECT_FILE.i:213.
+ Called from PROJECT_FILE.i:277.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- i <- main.
- Called from PROJECT_FILE.i:214.
+ Called from PROJECT_FILE.i:278.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- i <- main.
- Called from PROJECT_FILE.i:215.
+ Called from PROJECT_FILE.i:279.
[value] computing for function printf <- e_acsl_fail <- i <- 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 <- i <- 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 <- i <- main.
- Called from PROJECT_FILE.i:216.
+ Called from PROJECT_FILE.i:280.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- i <- main.
- Called from PROJECT_FILE.i:217.
+ Called from PROJECT_FILE.i:281.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- i <- 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 <- i <- main.
- Called from PROJECT_FILE.i:219.
+ Called from PROJECT_FILE.i:283.
[value] Done for function __gmpz_clear
[value] Recording results for i
[value] Done for function i
[value] computing for function j <- main.
- Called from PROJECT_FILE.i:449.
-PROJECT_FILE.i:227:[value] Function j, behavior b1: precondition got status valid.
-PROJECT_FILE.i:231:[value] Function j, behavior b2: precondition got status valid.
-PROJECT_FILE.i:232:[value] Function j, behavior b2: precondition got status valid.
+ Called from PROJECT_FILE.i:513.
+PROJECT_FILE.i:291:[value] Function j, behavior b1: precondition got status valid.
+PROJECT_FILE.i:295:[value] Function j, behavior b2: precondition got status valid.
+PROJECT_FILE.i:296:[value] Function j, behavior b2: precondition got status valid.
[value] computing for function __gmpz_init_set_si <- j <- main.
- Called from PROJECT_FILE.i:249.
+ Called from PROJECT_FILE.i:313.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- j <- main.
- Called from PROJECT_FILE.i:250.
+ Called from PROJECT_FILE.i:314.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- j <- main.
- Called from PROJECT_FILE.i:251.
+ Called from PROJECT_FILE.i:315.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- j <- main.
- Called from PROJECT_FILE.i:252.
+ Called from PROJECT_FILE.i:316.
[value] computing for function printf <- e_acsl_fail <- j <- 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 <- j <- 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_init_set_si <- j <- main.
- Called from PROJECT_FILE.i:253.
+ Called from PROJECT_FILE.i:317.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- j <- main.
- Called from PROJECT_FILE.i:254.
+ Called from PROJECT_FILE.i:318.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- j <- main.
- Called from PROJECT_FILE.i:255.
-PROJECT_FILE.i:21:[value] Function __gmpz_init: postcondition got status valid.
+ Called from PROJECT_FILE.i:319.
+PROJECT_FILE.i:63:[value] Function __gmpz_init: postcondition got status valid.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_add <- j <- main.
- Called from PROJECT_FILE.i:256.
-PROJECT_FILE.i:64:[value] Function __gmpz_add: precondition got status valid.
-PROJECT_FILE.i:65:[value] Function __gmpz_add: precondition got status valid.
-PROJECT_FILE.i:66:[value] Function __gmpz_add: precondition got status valid.
+ Called from PROJECT_FILE.i:320.
+PROJECT_FILE.i:106:[value] Function __gmpz_add: precondition got status valid.
+PROJECT_FILE.i:107:[value] Function __gmpz_add: precondition got status valid.
+PROJECT_FILE.i:108:[value] Function __gmpz_add: precondition got status valid.
[value] Done for function __gmpz_add
[value] computing for function __gmpz_cmp <- j <- main.
- Called from PROJECT_FILE.i:257.
+ Called from PROJECT_FILE.i:321.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- j <- main.
- Called from PROJECT_FILE.i:258.
+ Called from PROJECT_FILE.i:322.
[value] computing for function printf <- e_acsl_fail <- j <- 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 <- j <- 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_init_set_si <- j <- 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_cmp <- j <- main.
- Called from PROJECT_FILE.i:260.
+ Called from PROJECT_FILE.i:324.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- j <- main.
- Called from PROJECT_FILE.i:261.
+ Called from PROJECT_FILE.i:325.
[value] computing for function printf <- e_acsl_fail <- j <- 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 <- j <- 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 <- j <- main.
- Called from PROJECT_FILE.i:262.
+ Called from PROJECT_FILE.i:326.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- j <- main.
- Called from PROJECT_FILE.i:263.
+ Called from PROJECT_FILE.i:327.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- j <- 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 <- j <- 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 <- j <- main.
- Called from PROJECT_FILE.i:266.
+ Called from PROJECT_FILE.i:330.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- j <- main.
- Called from PROJECT_FILE.i:267.
+ Called from PROJECT_FILE.i:331.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_init_set_si <- j <- main.
- Called from PROJECT_FILE.i:279.
+ Called from PROJECT_FILE.i:343.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- j <- main.
- Called from PROJECT_FILE.i:280.
+ Called from PROJECT_FILE.i:344.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- j <- main.
- Called from PROJECT_FILE.i:281.
+ Called from PROJECT_FILE.i:345.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- j <- main.
- Called from PROJECT_FILE.i:282.
+ Called from PROJECT_FILE.i:346.
[value] computing for function printf <- e_acsl_fail <- j <- 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 <- j <- 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_init_set_si <- j <- main.
- Called from PROJECT_FILE.i:283.
+ Called from PROJECT_FILE.i:347.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- j <- main.
- Called from PROJECT_FILE.i:284.
+ Called from PROJECT_FILE.i:348.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- j <- main.
- Called from PROJECT_FILE.i:285.
+ Called from PROJECT_FILE.i:349.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_add <- j <- main.
- Called from PROJECT_FILE.i:286.
+ Called from PROJECT_FILE.i:350.
[value] Done for function __gmpz_add
[value] computing for function __gmpz_cmp <- j <- main.
- Called from PROJECT_FILE.i:287.
+ Called from PROJECT_FILE.i:351.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- j <- main.
- Called from PROJECT_FILE.i:288.
+ Called from PROJECT_FILE.i:352.
[value] computing for function printf <- e_acsl_fail <- j <- 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 <- j <- 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 <- j <- main.
- Called from PROJECT_FILE.i:289.
+ Called from PROJECT_FILE.i:353.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- j <- main.
- Called from PROJECT_FILE.i:290.
+ Called from PROJECT_FILE.i:354.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- j <- main.
- Called from PROJECT_FILE.i:291.
+ Called from PROJECT_FILE.i:355.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- j <- main.
- Called from PROJECT_FILE.i:292.
+ Called from PROJECT_FILE.i:356.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- j <- main.
- Called from PROJECT_FILE.i:293.
+ Called from PROJECT_FILE.i:357.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:228:[value] Function j, behavior b1: postcondition got status valid.
-PROJECT_FILE.i:233:[value] Function j, behavior b2: postcondition got status valid.
+PROJECT_FILE.i:292:[value] Function j, behavior b1: postcondition got status valid.
+PROJECT_FILE.i:297:[value] Function j, behavior b2: postcondition got status valid.
[value] Recording results for j
[value] Done for function j
[value] computing for function k <- main.
- Called from PROJECT_FILE.i:450.
-PROJECT_FILE.i:301:[value] Function k, behavior b1: assumption got status invalid; precondition not evaluated.
-PROJECT_FILE.i:306:[value] Function k, behavior b2: precondition got status valid.
-PROJECT_FILE.i:307:[value] Function k, behavior b2: precondition got status valid.
+ Called from PROJECT_FILE.i:514.
+PROJECT_FILE.i:365:[value] Function k, behavior b1: assumption got status invalid; precondition not evaluated.
+PROJECT_FILE.i:370:[value] Function k, behavior b2: precondition got status valid.
+PROJECT_FILE.i:371:[value] Function k, behavior b2: precondition got status valid.
[value] computing for function __gmpz_init_set_si <- k <- main.
- Called from PROJECT_FILE.i:325.
+ Called from PROJECT_FILE.i:389.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- k <- main.
- Called from PROJECT_FILE.i:326.
+ Called from PROJECT_FILE.i:390.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- k <- main.
- Called from PROJECT_FILE.i:327.
+ Called from PROJECT_FILE.i:391.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_init_set_si <- k <- main.
- Called from PROJECT_FILE.i:333.
+ Called from PROJECT_FILE.i:397.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- k <- main.
- Called from PROJECT_FILE.i:334.
+ Called from PROJECT_FILE.i:398.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- k <- main.
- Called from PROJECT_FILE.i:335.
+ Called from PROJECT_FILE.i:399.
[value] Done for function __gmpz_cmp
-PROJECT_FILE.i:336:[value] assigning non deterministic value for the first time
+PROJECT_FILE.i:400:[value] assigning non deterministic value for the first time
[value] computing for function __gmpz_clear <- k <- main.
- Called from PROJECT_FILE.i:337.
+ Called from PROJECT_FILE.i:401.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- k <- main.
- Called from PROJECT_FILE.i:338.
+ Called from PROJECT_FILE.i:402.
[value] Done for function __gmpz_clear
[value] computing for function e_acsl_fail <- k <- main.
- Called from PROJECT_FILE.i:340.
+ Called from PROJECT_FILE.i:404.
[value] computing for function printf <- e_acsl_fail <- k <- 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 <- k <- 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_init_set_si <- k <- main.
- Called from PROJECT_FILE.i:341.
+ Called from PROJECT_FILE.i:405.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- k <- main.
- Called from PROJECT_FILE.i:342.
+ Called from PROJECT_FILE.i:406.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_init_set_si <- k <- main.
- Called from PROJECT_FILE.i:347.
+ Called from PROJECT_FILE.i:411.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- k <- main.
- Called from PROJECT_FILE.i:348.
+ Called from PROJECT_FILE.i:412.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- k <- main.
- Called from PROJECT_FILE.i:349.
+ Called from PROJECT_FILE.i:413.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_clear <- k <- main.
- Called from PROJECT_FILE.i:351.
+ Called from PROJECT_FILE.i:415.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- k <- main.
- Called from PROJECT_FILE.i:352.
+ Called from PROJECT_FILE.i:416.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_init_set_si <- k <- main.
- Called from PROJECT_FILE.i:360.
+ Called from PROJECT_FILE.i:424.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- k <- main.
- Called from PROJECT_FILE.i:361.
+ Called from PROJECT_FILE.i:425.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- k <- main.
- Called from PROJECT_FILE.i:362.
+ Called from PROJECT_FILE.i:426.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_clear <- k <- main.
- Called from PROJECT_FILE.i:364.
+ Called from PROJECT_FILE.i:428.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- k <- main.
- Called from PROJECT_FILE.i:365.
+ Called from PROJECT_FILE.i:429.
[value] Done for function __gmpz_clear
[value] computing for function e_acsl_fail <- k <- main.
- Called from PROJECT_FILE.i:367.
+ Called from PROJECT_FILE.i:431.
[value] computing for function printf <- e_acsl_fail <- k <- 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 <- k <- 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_cmp <- k <- main.
- Called from PROJECT_FILE.i:368.
+ Called from PROJECT_FILE.i:432.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_init_set_si <- k <- main.
- Called from PROJECT_FILE.i:373.
+ Called from PROJECT_FILE.i:437.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- k <- main.
- Called from PROJECT_FILE.i:374.
+ Called from PROJECT_FILE.i:438.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- k <- main.
- Called from PROJECT_FILE.i:375.
+ Called from PROJECT_FILE.i:439.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_clear <- k <- main.
- Called from PROJECT_FILE.i:377.
+ Called from PROJECT_FILE.i:441.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- k <- main.
- Called from PROJECT_FILE.i:378.
+ Called from PROJECT_FILE.i:442.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_init_set_si <- k <- main.
- Called from PROJECT_FILE.i:388.
+ Called from PROJECT_FILE.i:452.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- k <- main.
- Called from PROJECT_FILE.i:389.
+ Called from PROJECT_FILE.i:453.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- k <- main.
- Called from PROJECT_FILE.i:390.
+ Called from PROJECT_FILE.i:454.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_add <- k <- main.
- Called from PROJECT_FILE.i:391.
+ Called from PROJECT_FILE.i:455.
[value] Done for function __gmpz_add
[value] computing for function __gmpz_init_set_si <- k <- main.
- Called from PROJECT_FILE.i:392.
+ Called from PROJECT_FILE.i:456.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- k <- main.
- Called from PROJECT_FILE.i:393.
+ Called from PROJECT_FILE.i:457.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_clear <- k <- main.
- Called from PROJECT_FILE.i:395.
+ Called from PROJECT_FILE.i:459.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- k <- main.
- Called from PROJECT_FILE.i:396.
+ Called from PROJECT_FILE.i:460.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- k <- main.
- Called from PROJECT_FILE.i:397.
+ Called from PROJECT_FILE.i:461.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- k <- main.
- Called from PROJECT_FILE.i:398.
+ Called from PROJECT_FILE.i:462.
[value] Done for function __gmpz_clear
[value] computing for function e_acsl_fail <- k <- main.
- Called from PROJECT_FILE.i:400.
+ Called from PROJECT_FILE.i:464.
[value] computing for function printf <- e_acsl_fail <- k <- 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 <- k <- 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 <- k <- main.
- Called from PROJECT_FILE.i:401.
+ Called from PROJECT_FILE.i:465.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- k <- main.
- Called from PROJECT_FILE.i:402.
+ Called from PROJECT_FILE.i:466.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- k <- main.
- Called from PROJECT_FILE.i:403.
+ Called from PROJECT_FILE.i:467.
[value] Done for function __gmpz_clear
[value] Recording results for k
[value] Done for function k
[value] computing for function l <- main.
- Called from PROJECT_FILE.i:451.
-PROJECT_FILE.i:413:[value] Assertion got status valid.
+ Called from PROJECT_FILE.i:515.
+PROJECT_FILE.i:477:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- l <- main.
- Called from PROJECT_FILE.i:418.
+ Called from PROJECT_FILE.i:482.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- l <- main.
- Called from PROJECT_FILE.i:419.
+ Called from PROJECT_FILE.i:483.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- l <- main.
- Called from PROJECT_FILE.i:420.
+ Called from PROJECT_FILE.i:484.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- l <- main.
- Called from PROJECT_FILE.i:421.
+ Called from PROJECT_FILE.i:485.
[value] computing for function printf <- e_acsl_fail <- l <- 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 <- l <- 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 <- l <- main.
- Called from PROJECT_FILE.i:422.
+ Called from PROJECT_FILE.i:486.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- l <- main.
- Called from PROJECT_FILE.i:423.
+ Called from PROJECT_FILE.i:487.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_init_set_si <- l <- main.
- Called from PROJECT_FILE.i:431.
+ Called from PROJECT_FILE.i:495.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- l <- main.
- Called from PROJECT_FILE.i:432.
+ Called from PROJECT_FILE.i:496.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- l <- main.
- Called from PROJECT_FILE.i:433.
+ Called from PROJECT_FILE.i:497.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- l <- main.
- Called from PROJECT_FILE.i:434.
+ Called from PROJECT_FILE.i:498.
[value] computing for function printf <- e_acsl_fail <- l <- 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 <- l <- 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 <- l <- main.
- Called from PROJECT_FILE.i:435.
+ Called from PROJECT_FILE.i:499.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- l <- main.
- Called from PROJECT_FILE.i:436.
+ Called from PROJECT_FILE.i:500.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:410:[value] Function l: postcondition got status valid.
+PROJECT_FILE.i:474:[value] Function l: postcondition got status valid.
[value] Recording results for l
[value] Done for function l
[value] Recording results for main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
index 92fbba22301..eccc463971b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
@@ -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
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
index 2744a9206e5..05717c8c131 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
@@ -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
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
index c19d36b485a..cd3a70c4d8e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
@@ -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
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
index c48528acf5d..d19f37d6739 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
@@ -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 ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle
index 265e6cabe40..ec190615b97 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle
@@ -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 ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
index 9b6270007a9..ea37edf7c2c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
@@ -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 ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
index 972b05cce49..ac8c48cf39b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
@@ -14,502 +14,502 @@ tests/e-acsl-runtime/ptr.i:26:[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:142:[value] Assertion got status valid.
+PROJECT_FILE.i:206:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:147.
-PROJECT_FILE.i:33:[value] Function __gmpz_init_set_si: postcondition got status valid.
+ Called from PROJECT_FILE.i:211.
+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:148.
+ Called from PROJECT_FILE.i:212.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:149.
-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:213.
+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:150.
+ Called from PROJECT_FILE.i:214.
[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] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:152.
+ Called from PROJECT_FILE.i:216.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:156:[value] Assertion got status valid.
+PROJECT_FILE.i:220:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:161.
+ Called from PROJECT_FILE.i:225.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:162.
+ Called from PROJECT_FILE.i:226.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:163.
+ Called from PROJECT_FILE.i:227.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:164.
+ Called from PROJECT_FILE.i:228.
[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:165.
+ Called from PROJECT_FILE.i:229.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:166.
+ Called from PROJECT_FILE.i:230.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:170:[value] Assertion got status valid.
+PROJECT_FILE.i:234:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- 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_init_set_si <- main.
- Called from PROJECT_FILE.i:176.
+ Called from PROJECT_FILE.i:240.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:177.
+ Called from PROJECT_FILE.i:241.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:178.
+ Called from PROJECT_FILE.i:242.
[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:179.
+ Called from PROJECT_FILE.i:243.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:180.
+ Called from PROJECT_FILE.i:244.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:184:[value] Assertion got status valid.
+PROJECT_FILE.i:248:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:197.
+ Called from PROJECT_FILE.i:261.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:198.
+ Called from PROJECT_FILE.i:262.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:199.
-PROJECT_FILE.i:21:[value] Function __gmpz_init: postcondition got status valid.
+ Called from PROJECT_FILE.i:263.
+PROJECT_FILE.i:63:[value] Function __gmpz_init: postcondition got status valid.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_mul <- main.
- Called from PROJECT_FILE.i:200.
-PROJECT_FILE.i:76:[value] Function __gmpz_mul: precondition got status valid.
-PROJECT_FILE.i:77:[value] Function __gmpz_mul: precondition got status valid.
-PROJECT_FILE.i:78:[value] Function __gmpz_mul: precondition got status valid.
+ Called from PROJECT_FILE.i:264.
+PROJECT_FILE.i:118:[value] Function __gmpz_mul: precondition got status valid.
+PROJECT_FILE.i:119:[value] Function __gmpz_mul: precondition got status valid.
+PROJECT_FILE.i:120:[value] Function __gmpz_mul: precondition got status valid.
[value] Done for function __gmpz_mul
[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_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_cmp <- main.
- Called from PROJECT_FILE.i:203.
+ Called from PROJECT_FILE.i:267.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:204.
+ Called from PROJECT_FILE.i:268.
[value] Done for function __gmpz_init
-PROJECT_FILE.i:205:[value] Assertion got status valid.
+PROJECT_FILE.i:269:[value] Assertion got status valid.
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:206.
+ Called from PROJECT_FILE.i:270.
[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_tdiv_q <- main.
- Called from PROJECT_FILE.i:207.
-PROJECT_FILE.i:82:[value] Function __gmpz_tdiv_q: precondition got status valid.
-PROJECT_FILE.i:83:[value] Function __gmpz_tdiv_q: precondition got status valid.
-PROJECT_FILE.i:84:[value] Function __gmpz_tdiv_q: precondition got status valid.
+ Called from PROJECT_FILE.i:271.
+PROJECT_FILE.i:124:[value] Function __gmpz_tdiv_q: precondition got status valid.
+PROJECT_FILE.i:125:[value] Function __gmpz_tdiv_q: precondition got status valid.
+PROJECT_FILE.i:126:[value] Function __gmpz_tdiv_q: precondition got status valid.
[value] Done for function __gmpz_tdiv_q
[value] computing for function __gmpz_get_si <- main.
- Called from PROJECT_FILE.i:208.
-PROJECT_FILE.i:96:[value] Function __gmpz_get_si: precondition got status valid.
+ Called from PROJECT_FILE.i:272.
+PROJECT_FILE.i:138:[value] Function __gmpz_get_si: precondition got status valid.
[value] Done for function __gmpz_get_si
-PROJECT_FILE.i:209:[kernel] warning: accessing out of bounds index [-2147483648..2147483647].
+PROJECT_FILE.i:273:[kernel] warning: accessing out of bounds index [-2147483648..2147483647].
assert 0 ≤ e_acsl_17 ∧ e_acsl_17 < 3;
[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:213.
+ Called from PROJECT_FILE.i:277.
[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:215.
+ Called from PROJECT_FILE.i:279.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:216.
+ Called from PROJECT_FILE.i:280.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:217.
+ Called from PROJECT_FILE.i:281.
[value] Done for function __gmpz_clear
[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
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:220.
+ Called from PROJECT_FILE.i:284.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:221.
+ Called from PROJECT_FILE.i:285.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:222.
+ Called from PROJECT_FILE.i:286.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:229:[value] entering loop for the first time
-PROJECT_FILE.i:232:[value] Assertion got status valid.
+PROJECT_FILE.i:293:[value] entering loop for the first time
+PROJECT_FILE.i:296:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:239.
+ Called from PROJECT_FILE.i:303.
[value] Done for function __gmpz_init_set_si
[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_set_si <- main.
- Called from PROJECT_FILE.i:241.
+ Called from PROJECT_FILE.i:305.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:242.
+ Called from PROJECT_FILE.i:306.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_add <- main.
- Called from PROJECT_FILE.i:243.
-PROJECT_FILE.i:64:[value] Function __gmpz_add: precondition got status valid.
-PROJECT_FILE.i:65:[value] Function __gmpz_add: precondition got status valid.
-PROJECT_FILE.i:66:[value] Function __gmpz_add: precondition got status valid.
+ Called from PROJECT_FILE.i:307.
+PROJECT_FILE.i:106:[value] Function __gmpz_add: precondition got status valid.
+PROJECT_FILE.i:107:[value] Function __gmpz_add: precondition got status valid.
+PROJECT_FILE.i:108:[value] Function __gmpz_add: precondition got status valid.
[value] Done for function __gmpz_add
[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
[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
-PROJECT_FILE.i:253:[value] Assertion got status valid.
+PROJECT_FILE.i:317:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:263.
+ Called from PROJECT_FILE.i:327.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:264.
+ Called from PROJECT_FILE.i:328.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:265.
+ Called from PROJECT_FILE.i:329.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_sub <- main.
- Called from PROJECT_FILE.i:266.
-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:330.
+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 <- main.
- Called from PROJECT_FILE.i:267.
+ Called from PROJECT_FILE.i:331.
[value] Done for function __gmpz_get_si
-PROJECT_FILE.i:268:[kernel] warning: accessing out of bounds index [-2147483648..2147483647].
+PROJECT_FILE.i:332:[kernel] warning: accessing out of bounds index [-2147483648..2147483647].
assert 0 ≤ e_acsl_29 ∧ e_acsl_29 < 3;
[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_init <- main.
- Called from PROJECT_FILE.i:270.
+ Called from PROJECT_FILE.i:334.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_sub <- main.
- Called from PROJECT_FILE.i:271.
+ Called from PROJECT_FILE.i:335.
[value] Done for function __gmpz_sub
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:272.
+ Called from PROJECT_FILE.i:336.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:273.
+ Called from PROJECT_FILE.i:337.
[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:274.
+ Called from PROJECT_FILE.i:338.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:275.
+ Called from PROJECT_FILE.i:339.
[value] Done for function __gmpz_clear
[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
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:278.
+ Called from PROJECT_FILE.i:342.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:279.
+ Called from PROJECT_FILE.i:343.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:283:[value] Assertion got status valid.
+PROJECT_FILE.i:347:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:290.
+ Called from PROJECT_FILE.i:354.
[value] Done for function __gmpz_init_set_si
[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_sub <- main.
- Called from PROJECT_FILE.i:294.
+ Called from PROJECT_FILE.i:358.
[value] Done for function __gmpz_sub
[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] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:300.
+ Called from PROJECT_FILE.i:364.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:232:[value] Assertion got status unknown.
+PROJECT_FILE.i:296:[value] Assertion got status unknown.
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:239.
+ Called from PROJECT_FILE.i:303.
[value] Done for function __gmpz_init_set_si
[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_set_si <- main.
- Called from PROJECT_FILE.i:241.
+ Called from PROJECT_FILE.i:305.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:242.
+ Called from PROJECT_FILE.i:306.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_add <- main.
- Called from PROJECT_FILE.i:243.
+ Called from PROJECT_FILE.i:307.
[value] Done for function __gmpz_add
[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
[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
-PROJECT_FILE.i:253:[value] Assertion got status unknown.
+PROJECT_FILE.i:317:[value] Assertion got status unknown.
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:263.
+ Called from PROJECT_FILE.i:327.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:264.
+ Called from PROJECT_FILE.i:328.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:265.
+ Called from PROJECT_FILE.i:329.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_sub <- main.
- Called from PROJECT_FILE.i:266.
+ Called from PROJECT_FILE.i:330.
[value] Done for function __gmpz_sub
[value] computing for function __gmpz_get_si <- main.
- Called from PROJECT_FILE.i:267.
+ Called from PROJECT_FILE.i:331.
[value] Done for function __gmpz_get_si
-PROJECT_FILE.i:268:[value] Assertion got status unknown.
+PROJECT_FILE.i:332:[value] Assertion got status unknown.
[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_init <- main.
- Called from PROJECT_FILE.i:270.
+ Called from PROJECT_FILE.i:334.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_sub <- main.
- Called from PROJECT_FILE.i:271.
+ Called from PROJECT_FILE.i:335.
[value] Done for function __gmpz_sub
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:272.
+ Called from PROJECT_FILE.i:336.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:273.
+ Called from PROJECT_FILE.i:337.
[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:274.
+ Called from PROJECT_FILE.i:338.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:275.
+ Called from PROJECT_FILE.i:339.
[value] Done for function __gmpz_clear
[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
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:278.
+ Called from PROJECT_FILE.i:342.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:279.
+ Called from PROJECT_FILE.i:343.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:283:[value] Assertion got status unknown.
+PROJECT_FILE.i:347:[value] Assertion got status unknown.
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:290.
+ Called from PROJECT_FILE.i:354.
[value] Done for function __gmpz_init_set_si
[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_sub <- main.
- Called from PROJECT_FILE.i:294.
+ Called from PROJECT_FILE.i:358.
[value] Done for function __gmpz_sub
[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] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:300.
+ Called from PROJECT_FILE.i:364.
[value] Done for function __gmpz_clear
-PROJECT_FILE.i:304:[value] assigning non deterministic value for the first time
-PROJECT_FILE.i:310:[value] Assertion got status valid.
+PROJECT_FILE.i:368:[value] assigning non deterministic value for the first time
+PROJECT_FILE.i:374:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:315.
+ Called from PROJECT_FILE.i:379.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:316.
+ Called from PROJECT_FILE.i:380.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:317.
+ Called from PROJECT_FILE.i:381.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:318.
+ Called from PROJECT_FILE.i:382.
[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:319.
+ Called from PROJECT_FILE.i:383.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:320.
+ Called from PROJECT_FILE.i:384.
[value] Done for function __gmpz_clear
[value] Recording results for main
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
index 5f62bd3b13f..55ca70cc6bf 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
@@ -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
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
index 098bbf627fb..466a48e0381 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
@@ -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
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
index ebe5dc9303a..155078ff222 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
@@ -3,542 +3,542 @@
[value] Initial state computed
[value] Values of globals at initialization
[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 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
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:149.
+ Called from PROJECT_FILE.i:213.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:161.
+ Called from PROJECT_FILE.i:225.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:162.
+ Called from PROJECT_FILE.i:226.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:163.
+ Called from PROJECT_FILE.i:227.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:164.
+ Called from PROJECT_FILE.i:228.
[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_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
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:170.
+ Called from PROJECT_FILE.i:234.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:178.
+ Called from PROJECT_FILE.i:242.
[value] Done for function __gmpz_init_set_si
[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
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:180.
+ Called from PROJECT_FILE.i:244.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:181.
+ Called from PROJECT_FILE.i:245.
[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:182.
+ Called from PROJECT_FILE.i:246.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:183.
+ Called from PROJECT_FILE.i:247.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:196.
+ Called from PROJECT_FILE.i:260.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:197.
+ Called from PROJECT_FILE.i:261.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:198.
+ Called from PROJECT_FILE.i:262.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:199.
+ Called from PROJECT_FILE.i:263.
[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_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_clear <- main.
- Called from PROJECT_FILE.i:206.
+ Called from PROJECT_FILE.i:270.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:207.
+ Called from PROJECT_FILE.i:271.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:239.
+ Called from PROJECT_FILE.i:303.
[value] Done for function __gmpz_init_set_si
[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_cmp <- main.
- Called from PROJECT_FILE.i:241.
+ Called from PROJECT_FILE.i:305.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:242.
+ Called from PROJECT_FILE.i:306.
[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_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_init_set_si <- main.
- Called from PROJECT_FILE.i:244.
+ Called from PROJECT_FILE.i:308.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:245.
-PROJECT_FILE.i:21:[value] Function __gmpz_init: postcondition got status valid.
+ Called from PROJECT_FILE.i:309.
+PROJECT_FILE.i:63:[value] Function __gmpz_init: postcondition got status valid.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_add <- main.
- Called from PROJECT_FILE.i:246.
-PROJECT_FILE.i:64:[value] Function __gmpz_add: precondition got status valid.
-PROJECT_FILE.i:65:[value] Function __gmpz_add: precondition got status valid.
-PROJECT_FILE.i:66:[value] Function __gmpz_add: precondition got status valid.
+ Called from PROJECT_FILE.i:310.
+PROJECT_FILE.i:106:[value] Function __gmpz_add: precondition got status valid.
+PROJECT_FILE.i:107:[value] Function __gmpz_add: precondition got status valid.
+PROJECT_FILE.i:108:[value] Function __gmpz_add: precondition got status valid.
[value] Done for function __gmpz_add
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:247.
+ Called from PROJECT_FILE.i:311.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:248.
+ Called from PROJECT_FILE.i:312.
[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_init_set_si <- main.
- Called from PROJECT_FILE.i:249.
+ Called from PROJECT_FILE.i:313.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:250.
+ Called from PROJECT_FILE.i:314.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:251.
+ Called from PROJECT_FILE.i:315.
[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:252.
+ Called from PROJECT_FILE.i:316.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:253.
+ Called from PROJECT_FILE.i:317.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:254.
+ Called from PROJECT_FILE.i:318.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:255.
+ Called from PROJECT_FILE.i:319.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:256.
+ Called from PROJECT_FILE.i:320.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:257.
+ Called from PROJECT_FILE.i:321.
[value] Done for function __gmpz_clear
[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_init_set_si <- main.
- Called from PROJECT_FILE.i:262.
+ Called from PROJECT_FILE.i:326.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:263.
+ Called from PROJECT_FILE.i:327.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:264.
+ Called from PROJECT_FILE.i:328.
[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_init_set_si <- main.
- Called from PROJECT_FILE.i:265.
+ Called from PROJECT_FILE.i:329.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:266.
+ Called from PROJECT_FILE.i:330.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:267.
+ Called from PROJECT_FILE.i:331.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_add <- main.
- Called from PROJECT_FILE.i:268.
+ Called from PROJECT_FILE.i:332.
[value] Done for function __gmpz_add
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:269.
+ Called from PROJECT_FILE.i:333.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:270.
+ Called from PROJECT_FILE.i:334.
[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:271.
+ Called from PROJECT_FILE.i:335.
[value] Done for function __gmpz_clear
[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 __gmpz_clear <- main.
- Called from PROJECT_FILE.i:274.
+ Called from PROJECT_FILE.i:338.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:275.
+ Called from PROJECT_FILE.i:339.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:301.
+ Called from PROJECT_FILE.i:365.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:302.
+ Called from PROJECT_FILE.i:366.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:303.
+ Called from PROJECT_FILE.i:367.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:309.
+ Called from PROJECT_FILE.i:373.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:310.
+ Called from PROJECT_FILE.i:374.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:311.
+ Called from PROJECT_FILE.i:375.
[value] Done for function __gmpz_cmp
-PROJECT_FILE.i:312:[value] assigning non deterministic value for the first time
+PROJECT_FILE.i:376:[value] assigning non deterministic value for the first time
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:313.
+ Called from PROJECT_FILE.i:377.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:314.
+ Called from PROJECT_FILE.i:378.
[value] Done for function __gmpz_clear
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:316.
+ Called from PROJECT_FILE.i:380.
[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_init_set_si <- main.
- Called from PROJECT_FILE.i:317.
+ Called from PROJECT_FILE.i:381.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:318.
+ Called from PROJECT_FILE.i:382.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:323.
+ Called from PROJECT_FILE.i:387.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:324.
+ Called from PROJECT_FILE.i:388.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:325.
+ Called from PROJECT_FILE.i:389.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:327.
+ Called from PROJECT_FILE.i:391.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:328.
+ Called from PROJECT_FILE.i:392.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:336.
+ Called from PROJECT_FILE.i:400.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:337.
+ Called from PROJECT_FILE.i:401.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:338.
+ Called from PROJECT_FILE.i:402.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:340.
+ Called from PROJECT_FILE.i:404.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:341.
+ Called from PROJECT_FILE.i:405.
[value] Done for function __gmpz_clear
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:343.
+ Called from PROJECT_FILE.i:407.
[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_cmp <- main.
- Called from PROJECT_FILE.i:344.
+ Called from PROJECT_FILE.i:408.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:349.
+ Called from PROJECT_FILE.i:413.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:350.
+ Called from PROJECT_FILE.i:414.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:351.
+ Called from PROJECT_FILE.i:415.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:353.
+ Called from PROJECT_FILE.i:417.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:354.
+ Called from PROJECT_FILE.i:418.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:364.
+ Called from PROJECT_FILE.i:428.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:365.
+ Called from PROJECT_FILE.i:429.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- main.
- Called from PROJECT_FILE.i:366.
+ Called from PROJECT_FILE.i:430.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_add <- main.
- Called from PROJECT_FILE.i:367.
+ Called from PROJECT_FILE.i:431.
[value] Done for function __gmpz_add
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:368.
+ Called from PROJECT_FILE.i:432.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:369.
+ Called from PROJECT_FILE.i:433.
[value] Done for function __gmpz_cmp
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:371.
+ Called from PROJECT_FILE.i:435.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:372.
+ Called from PROJECT_FILE.i:436.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:373.
+ Called from PROJECT_FILE.i:437.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:374.
+ Called from PROJECT_FILE.i:438.
[value] Done for function __gmpz_clear
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:376.
+ Called from PROJECT_FILE.i:440.
[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:377.
+ Called from PROJECT_FILE.i:441.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:378.
+ Called from PROJECT_FILE.i:442.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:379.
+ Called from PROJECT_FILE.i:443.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:388.
+ Called from PROJECT_FILE.i:452.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:389.
+ Called from PROJECT_FILE.i:453.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:390.
+ Called from PROJECT_FILE.i:454.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:391.
+ Called from PROJECT_FILE.i:455.
[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:392.
+ Called from PROJECT_FILE.i:456.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:393.
+ Called from PROJECT_FILE.i:457.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:399.
+ Called from PROJECT_FILE.i:463.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:400.
+ Called from PROJECT_FILE.i:464.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:401.
+ Called from PROJECT_FILE.i:465.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:402.
+ Called from PROJECT_FILE.i:466.
[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:403.
+ Called from PROJECT_FILE.i:467.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:404.
+ Called from PROJECT_FILE.i:468.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:419.
+ Called from PROJECT_FILE.i:483.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:420.
+ Called from PROJECT_FILE.i:484.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:421.
+ Called from PROJECT_FILE.i:485.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:422.
+ Called from PROJECT_FILE.i:486.
[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:423.
+ Called from PROJECT_FILE.i:487.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:424.
+ Called from PROJECT_FILE.i:488.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:428.
+ Called from PROJECT_FILE.i:492.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from PROJECT_FILE.i:429.
+ Called from PROJECT_FILE.i:493.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from PROJECT_FILE.i:430.
+ Called from PROJECT_FILE.i:494.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:431.
+ Called from PROJECT_FILE.i:495.
[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:432.
+ Called from PROJECT_FILE.i:496.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from PROJECT_FILE.i:433.
+ Called from PROJECT_FILE.i:497.
[value] Done for function __gmpz_clear
[value] Recording results for main
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
index 6f641f5decb..befe0072061 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
@@ -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 ======
--
GitLab