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

[E-ACSL] configure the memory model's C library with the Frama-C's machdep

parent 1ff9db31
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 120 additions and 116 deletions
src/plugins/e-acsl/main.ml
+ 3
− 1
View file @ 4308b243
......@@ -54,7 +54,9 @@ module Extended_ast =
let unmemoized_extend_ast () =
let extend () =
Kernel.CppExtraArgs.add
(Pretty_utils.sfprintf " -I%s/libc" Config.datadir);
(Pretty_utils.sfprintf " -DE_ACSL_MACHDEP=%s -I%s/libc"
(Kernel.Machdep.get ())
Config.datadir);
Kernel.Keep_unused_specified_functions.off ();
let register s =
File.pre_register
......
src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
+ 14
− 10
View file @ 4308b243
#include <assert.h>
#include <errno.h>
#include <unistd.h>
......@@ -7,7 +6,6 @@
#include "e_acsl_bittree.h"
#include "e_acsl_mmodel.h"
#if WORDBITS == 16
unsigned long Tmasks[] =
......@@ -69,9 +67,13 @@ unsigned long Tmasks[] = {
0xfffffffe,
0xffffffff};
int Teq[] = {0,-1,3,-3,6,-5,7,-7,12,-9,11,-11,14,-13,15,-15,24,-17,19,-19,22,-21,23,-23,28,-25,27,-27,30,-29,31,32,-32};
int Tneq[] = {0,0,1,-2,2,-4,5,-6,4,-8,9,-10,10,-12,13,-14,8,-16,17,-18,18,-20,21,-22,20,-24,25,-26,26,-28,29,-30,-31};
int Teq[] =
{ 0,-1,3,-3,6,-5,7,-7,12,-9,11,-11,14,-13,15,-15,24,-17,19,-19,22,
-21,23,-23,28,-25,27,-27,30,-29,31,32,-32 };
int Tneq[] =
{ 0,0,1,-2,2,-4,5,-6,4,-8,9,-10,10,-12,13,-14,8,-16,17,-18,18,-20,21,-22,20,
-24,25,-26,26,-28,29,-30,-31 };
#else /* WORDBITS == 64 */
......@@ -143,15 +145,18 @@ unsigned long Tmasks[] = {
0xffffffffffffffff};
int Teq[] = {0,-1,3,-3,6,-5,7,-7,12,-9,11,-11,14,-13,15,-15,24,-17,19,-19,22,-21,23,-23,28,-25,27,-27,30,-29,31,-31,48,-33,35,-35,38,-37,39,-39,44,-41,43,-43,46,-45,47,-47,56,-49,51,-51,54,-53,55,-55,60,-57,59,-59,62,-61,63,64,-64};
int Teq[] =
{ 0,-1,3,-3,6,-5,7,-7,12,-9,11,-11,14,-13,15,-15,24,-17,19,-19,22,-21,23,-23,
28,-25,27,-27,30,-29,31,-31,48,-33,35,-35,38,-37,39,-39,44,-41,43,-43,46,
-45,47,-47,56,-49,51,-51,54,-53,55,-55,60,-57,59,-59,62,-61,63,64,-64 };
int Tneq[] = {0,0,1,-2,2,-4,5,-6,4,-8,9,-10,10,-12,13,-14,8,-16,17,-18,18,-20,21,-22,20,-24,25,-26,26,-28,29,-30,16,-32,33,-34,34,-36,37,-38,36,-40,41,-42,42,-44,45,-46,40,-48,49,-50,50,-52,53,-54,52,-56,57,-58,58,-60,61,-62,-63};
int Tneq[] =
{ 0,0,1,-2,2,-4,5,-6,4,-8,9,-10,10,-12,13,-14,8,-16,17,-18,18,-20,21,-22,20,
-24,25,-26,26,-28,29,-30,16,-32,33,-34,34,-36,37,-38,36,-40,41,-42,42,-44,
45,-46,40,-48,49,-50,50,-52,53,-54,52,-56,57,-58,58,-60,61,-62,-63 };
#endif
struct bittree {
int is_leaf;
char* addr;
......@@ -441,4 +446,3 @@ void __debug_struct () {
__debug_rec(__root);
printf("\t\t\t-----------------\n");
}
src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h
+ 1
− 3
View file @ 4308b243
......@@ -4,7 +4,6 @@
#include "stdlib.h"
#include "stdbool.h"
#if E_ACSL_MACHDEP == x86_64
#define WORDBITS 64
#elif E_ACSL_MACHDEP == x86_32
......@@ -14,10 +13,9 @@
#elif E_ACSL_MACHDEP == x86_16
#define WORDBITS 16
#else
#define WORDBITS 64
#define WORDBITS 32
#endif
/* Memory block allocated and may be deallocated */
struct _block {
char * ptr; /* begin address */
......
src/plugins/e-acsl/tests/e-acsl-reject/oracle/quantif.res.oracle
+ 6
− 6
View file @ 4308b243
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
tests/e-acsl-reject/quantif.i:6:[e-acsl] warning: E-ACSL construct `unguarded \forall quantification' is not yet supported.
Ignoring annotation.
tests/e-acsl-reject/quantif.i:7:[e-acsl] warning: invalid E-ACSL construct
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle
+ 6
− 6
View file @ 4308b243
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
+ 6
− 6
View file @ 4308b243
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
+ 6
− 6
View file @ 4308b243
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
+ 6
− 6
View file @ 4308b243
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
+ 6
− 6
View file @ 4308b243
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
+ 6
− 6
View file @ 4308b243
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
+ 6
− 6
View file @ 4308b243
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
+ 6
− 6
View file @ 4308b243
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
+ 6
− 6
View file @ 4308b243
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle
+ 6
− 6
View file @ 4308b243
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
+ 6
− 6
View file @ 4308b243
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
tests/e-acsl-runtime/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
tests/e-acsl-runtime/bts1307.i:31:[e-acsl] warning: approximating type `real' by `long double'
tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
+ 6
− 6
View file @ 4308b243
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
tests/e-acsl-runtime/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
tests/e-acsl-runtime/bts1307.i:31:[e-acsl] warning: approximating type `real' by `long double'
tests/e-acsl-runtime/bts1307.i:31:[e-acsl] approximating a real number by a float
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
+ 6
− 6
View file @ 4308b243
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
tests/e-acsl-runtime/bts1324.i:8:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
tests/e-acsl-runtime/bts1324.i:8:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
[value] Analyzing a complete application starting at main
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
+ 6
− 6
View file @ 4308b243
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.res.oracle
+ 6
− 6
View file @ 4308b243
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.res.oracle
+ 6
− 6
View file @ 4308b243
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment