From c079a19e06f481ef5ba078165e07be4ce6bacfeb Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 30 May 2013 09:09:21 +0000
Subject: [PATCH] [E-ACSL] add demo [E-ACSL] fixed bug in debug mode [E-ACSL]
add missing headers
---
src/plugins/e-acsl/Makefile.in | 2 +-
src/plugins/e-acsl/TODO | 23 ++--
src/plugins/e-acsl/demo/TODO | 1 +
src/plugins/e-acsl/demo/alone.sh | 2 +
src/plugins/e-acsl/demo/clean.sh | 5 +
src/plugins/e-acsl/demo/compile.sh | 2 +
src/plugins/e-acsl/demo/demo.c | 29 +++++
src/plugins/e-acsl/demo/demo.sh | 2 +
src/plugins/e-acsl/demo/load.sh | 3 +
src/plugins/e-acsl/demo/my_e_acsl.c | 50 ++++++++
src/plugins/e-acsl/demo/pow.c | 11 ++
src/plugins/e-acsl/demo/run_demo.sh | 7 ++
src/plugins/e-acsl/demo/run_script.sh | 7 ++
src/plugins/e-acsl/demo/script.ml | 116 ++++++++++++++++++
src/plugins/e-acsl/doc/Changelog | 6 +
src/plugins/e-acsl/gcc.sh | 3 +
src/plugins/e-acsl/misc.ml | 7 +-
src/plugins/e-acsl/share/e-acsl/e_acsl.c | 2 +-
.../e-acsl/memory_model/e_acsl_bittree.c | 22 ++++
.../e-acsl/memory_model/e_acsl_bittree.h | 22 ++++
.../share/e-acsl/memory_model/e_acsl_mmodel.c | 24 +++-
.../share/e-acsl/memory_model/e_acsl_mmodel.h | 21 ++++
.../e-acsl/memory_model/e_acsl_mmodel_api.h | 22 ++++
.../e-acsl-runtime/oracle/addrOf.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/addrOf.res.oracle | 4 +-
.../oracle/bts1304.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/bts1304.res.oracle | 4 +-
.../oracle/bts1399.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/bts1399.res.oracle | 4 +-
.../e-acsl-runtime/oracle/ghost.1.res.oracle | 4 +-
.../oracle/literal_string.1.res.oracle | 4 +-
.../oracle/literal_string.res.oracle | 4 +-
.../oracle/localvar.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/localvar.res.oracle | 4 +-
.../e-acsl-runtime/oracle/ptr.res.oracle | 4 +-
.../oracle/ptr_init.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/ptr_init.res.oracle | 4 +-
.../e-acsl-runtime/oracle/valid.1.res.oracle | 6 +-
.../e-acsl-runtime/oracle/valid.res.oracle | 6 +-
.../oracle/valid_alias.1.res.oracle | 6 +-
.../oracle/valid_alias.res.oracle | 6 +-
.../oracle/valid_in_contract.1.res.oracle | 4 +-
.../oracle/valid_in_contract.res.oracle | 4 +-
.../e-acsl-runtime/oracle/vector.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/vector.res.oracle | 4 +-
45 files changed, 419 insertions(+), 66 deletions(-)
create mode 100644 src/plugins/e-acsl/demo/TODO
create mode 100755 src/plugins/e-acsl/demo/alone.sh
create mode 100755 src/plugins/e-acsl/demo/clean.sh
create mode 100755 src/plugins/e-acsl/demo/compile.sh
create mode 100644 src/plugins/e-acsl/demo/demo.c
create mode 100755 src/plugins/e-acsl/demo/demo.sh
create mode 100755 src/plugins/e-acsl/demo/load.sh
create mode 100644 src/plugins/e-acsl/demo/my_e_acsl.c
create mode 100644 src/plugins/e-acsl/demo/pow.c
create mode 100755 src/plugins/e-acsl/demo/run_demo.sh
create mode 100755 src/plugins/e-acsl/demo/run_script.sh
create mode 100644 src/plugins/e-acsl/demo/script.ml
create mode 100755 src/plugins/e-acsl/gcc.sh
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 416bd00dea1..3f0b0096fb0 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -205,7 +205,7 @@ headers::
headache -c license/headache_config.txt -h license/CEA_LGPL \
*.ml *.mli \
Makefile.in configure.ac \
- share/e-acsl/*.h
+ share/e-acsl/*.[ch] share/e-acsl/*/*.[ch]
################
# Generic part #
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 44186c8829c..4c64d0ff83c 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -5,27 +5,28 @@
- [Bernard] avoir une fonction e_acsl_trace_behavior(char *bhv_name) {}
à appeler dès qu'un behavior est activé
- [Yannick] Logic functions
+- [Nikolaï] temporal memory properties
+- memory profiling
#####################
# E-ACSL CONSTRUCTS #
#####################
+- assigns, loop assigns
- predicates
- logic functions
- disjoint and complete behaviors (cf. Bernard's feature wish)
- loop invariant
- loop variant
+- grep "not_yet" *.ml
########
# CODE #
########
- grep TODO *.ml*
-- Gestion du mode -lib-entry et/ou pas de main
-- variable GMP potentiellement initialisée mais non utilisée en présence de \at
- (voir test result.i, cas -e-acsl-gmp-only)
+- Gestion du mode -lib-entry
- générer les delete des globals dans une fonction séparée, comme pour les init.
-- variadic functions are not yet duplicated
- generate guard for \offset, \block_length and \base_addr
(\offset(p) must ensures that p is valid)
- don't generate code for properties with status valid_under_hyp when we know
@@ -40,12 +41,16 @@
- analysis: fixed incorrectness in presence of recursive functions
- RTE: potential duplication (e.g. with **p)
- default output of e_acsl_assert in the format of standart error messages
+- some calls to __eacsl_memory_debug are missing in debug mode
##############
# KNOWN BUGS #
##############
- see BTS
+- see Chapter "Known Limitations" of the User Manual
+- variable GMP potentiellement initialisée mais non utilisée en présence de \at
+ (voir test result.i, cas -e-acsl-gmp-only)
- comparaisons qui aboutissent à du C incorrect
==> comparaison de chaînes litérales
(voir tests other_constants.i et comparison.i)
@@ -57,21 +62,17 @@
- incorrect d'utiliser Pre, Post, Here, Old dans stmt contract
(même problème que Jessie: cf. BTS #72)
(voir aussi result.i et ./at_stmt_contract.i)
-- interprétation des tableaux
-- \valid (or other memory-model constructs) in ensures of functions without code
-- function pointers
- (in case of the pointing function has a behavior like in test ptr_init.c)
+- interprétation des tableaux logiques
+[Dillon] Windows
#######
# DOC #
#######
-- write user manual
-- update according to the latest version of ACSL
-
#########
# TESTS #
#########
- inclure exemple du E-ACSL Reference Manual
+- inclure exemple du E-ACSL User Manual
- test arith.i: mettre les exemples du ACSL manual about div and modulo
diff --git a/src/plugins/e-acsl/demo/TODO b/src/plugins/e-acsl/demo/TODO
new file mode 100644
index 00000000000..eb262653db9
--- /dev/null
+++ b/src/plugins/e-acsl/demo/TODO
@@ -0,0 +1 @@
+les TODO et assert false dans script.ml
diff --git a/src/plugins/e-acsl/demo/alone.sh b/src/plugins/e-acsl/demo/alone.sh
new file mode 100755
index 00000000000..bbe34a54cc2
--- /dev/null
+++ b/src/plugins/e-acsl/demo/alone.sh
@@ -0,0 +1,2 @@
+#! /bin/sh
+frama-c demo.c -e-acsl -then-on e-acsl -print -ocode res_demo.c
diff --git a/src/plugins/e-acsl/demo/clean.sh b/src/plugins/e-acsl/demo/clean.sh
new file mode 100755
index 00000000000..857fa369f07
--- /dev/null
+++ b/src/plugins/e-acsl/demo/clean.sh
@@ -0,0 +1,5 @@
+#!/bin/bash
+
+clean
+rm -f demo.sav demo script frama_c_journal.ml res_demo.c
+./compile.sh
diff --git a/src/plugins/e-acsl/demo/compile.sh b/src/plugins/e-acsl/demo/compile.sh
new file mode 100755
index 00000000000..8f56bda68fe
--- /dev/null
+++ b/src/plugins/e-acsl/demo/compile.sh
@@ -0,0 +1,2 @@
+#!/bin/sh
+ocamlopt.opt -shared -o ./Script.cmxs -w Ly -warn-error A -I /usr/local/lib/frama-c -I . script.ml
diff --git a/src/plugins/e-acsl/demo/demo.c b/src/plugins/e-acsl/demo/demo.c
new file mode 100644
index 00000000000..2b5cc8f7e25
--- /dev/null
+++ b/src/plugins/e-acsl/demo/demo.c
@@ -0,0 +1,29 @@
+/*@ assigns \nothing;
+ @ behavior even:
+ @ assumes m % 2 == 0;
+ @ ensures \result >= 1;
+ @ behavior odd:
+ @ assumes m % 2 != 0;
+ @ ensures n >= 0 ==> \result >= 1;
+ @ ensures n < 0 ==> \result <= -1; */
+int pow(int n, unsigned int m);
+
+int sum(int x) {
+ int n = 0, i;
+ for(i = 1; i <= x; i++) n += i;
+ return n;
+}
+
+int main(void) {
+ int i, n = 0;
+ unsigned int a[100];
+ n = sum(10);
+ /*@ loop invariant 0 <= i <= n ;
+ @ loop invariant \forall integer k; 0 <= k < i ==> a[k] >= 1;
+ @ loop assigns i,a[0..n-1]; */
+ for(i = 0; i < n; i++) {
+ int tmp = pow(i, i);
+ a[i] = tmp;
+ }
+ /*@ assert \forall integer k; 0 <= k < n ==> a[k] >= 1; */
+}
diff --git a/src/plugins/e-acsl/demo/demo.sh b/src/plugins/e-acsl/demo/demo.sh
new file mode 100755
index 00000000000..a8529b2966a
--- /dev/null
+++ b/src/plugins/e-acsl/demo/demo.sh
@@ -0,0 +1,2 @@
+#! /bin/sh
+frama-c -e-acsl-prepare -save demo.sav demo.c -wp -then -val -slevel 11 -then -e-acsl -then-on e-acsl -print -ocode res_demo.c
diff --git a/src/plugins/e-acsl/demo/load.sh b/src/plugins/e-acsl/demo/load.sh
new file mode 100755
index 00000000000..ba15ee82137
--- /dev/null
+++ b/src/plugins/e-acsl/demo/load.sh
@@ -0,0 +1,3 @@
+#!/bin/bash
+
+frama-c-gui -load demo.sav
diff --git a/src/plugins/e-acsl/demo/my_e_acsl.c b/src/plugins/e-acsl/demo/my_e_acsl.c
new file mode 100644
index 00000000000..c3175d2b822
--- /dev/null
+++ b/src/plugins/e-acsl/demo/my_e_acsl.c
@@ -0,0 +1,50 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include <sys/types.h>
+#include <sys/wait.h>
+#include <unistd.h>
+
+#define LEN 10
+int LAST[LEN] = { -1, -1, -1, -1, -1, -1, -1, -1, -1, -1 };
+int IDX = 0;
+
+int mem(int x) {
+ for(int i = 0; i < LEN; i++)
+ if (LAST[i] == x) return x;
+ return -1;
+}
+
+void e_acsl_assert(int predicate,
+ char *kind,
+ char *fct,
+ char *pred_txt,
+ int line)
+{
+ if (! predicate) {
+ if (mem(line) == -1) {
+ LAST[IDX] = line;
+ IDX++;
+ int cpid = fork ();
+ if (cpid < 0) {
+ printf("%s failed at line %d of function %s.\n \
+The failing predicate is:\n%s.\n",
+ kind, line, fct, pred_txt);
+ } else {
+ int status;
+ if (cpid == 0) {
+ char *line_string = (char*) malloc(sizeof(char)*3);
+ sprintf(line_string,"%d",line);
+ char *args[17] = { "frama-c", "-quiet",
+ "-load", "demo.sav", "-save", "demo.sav",
+ "-load-module", "./Script", "-t2p-verbose", "1",
+ "-ppt-fct", fct,
+ "-ppt-name", kind,
+ "-ppt-line", line_string };
+ status = execvp("frama-c", args);
+ exit(status);
+ } else
+ wait(&status);
+ }
+ }
+ }
+}
diff --git a/src/plugins/e-acsl/demo/pow.c b/src/plugins/e-acsl/demo/pow.c
new file mode 100644
index 00000000000..a7715ec30ec
--- /dev/null
+++ b/src/plugins/e-acsl/demo/pow.c
@@ -0,0 +1,11 @@
+#include "stdio.h"
+
+int pow(int x, unsigned int n) {
+ unsigned int res = 1;
+ while (n) {
+ if (n & 1) res *= x;
+ n >>= 1;
+ x *= x;
+ }
+ return res;
+}
diff --git a/src/plugins/e-acsl/demo/run_demo.sh b/src/plugins/e-acsl/demo/run_demo.sh
new file mode 100755
index 00000000000..f110b94f001
--- /dev/null
+++ b/src/plugins/e-acsl/demo/run_demo.sh
@@ -0,0 +1,7 @@
+#! /bin/sh
+
+E_ACSL_LIB=`frama-c -print-share-path`/e-acsl
+
+gcc -std=c99 -pedantic -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin -o ./demo pow.c $E_ACSL_LIB/e_acsl.c $E_ACSL_LIB/memory_model/e_acsl_bittree.c $E_ACSL_LIB/memory_model/e_acsl_mmodel.c res_demo.c
+
+./demo
diff --git a/src/plugins/e-acsl/demo/run_script.sh b/src/plugins/e-acsl/demo/run_script.sh
new file mode 100755
index 00000000000..e5d1fd94248
--- /dev/null
+++ b/src/plugins/e-acsl/demo/run_script.sh
@@ -0,0 +1,7 @@
+#! /bin/sh
+
+E_ACSL_LIB=`frama-c -print-share-path`/e-acsl
+
+gcc -std=c99 -pedantic -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin -o ./script pow.c my_e_acsl.c $E_ACSL_LIB/memory_model/e_acsl_bittree.c $E_ACSL_LIB/memory_model/e_acsl_mmodel.c res_demo.c
+
+./script
diff --git a/src/plugins/e-acsl/demo/script.ml b/src/plugins/e-acsl/demo/script.ml
new file mode 100644
index 00000000000..37558dbeaaa
--- /dev/null
+++ b/src/plugins/e-acsl/demo/script.ml
@@ -0,0 +1,116 @@
+open Cil_types
+
+(* ************************************************************************** *)
+(* Registering the plug-in *)
+(* ************************************************************************** *)
+
+include Plugin.Register(struct
+ let name = "txt2ppt"
+ let shortname = "t2p"
+ let help = "Convert E-ACSL textual properties to Frama-C properties"
+end)
+
+(* ************************************************************************** *)
+(* Defining plug-in's options *)
+(* ************************************************************************** *)
+
+module Fct_name =
+ EmptyString
+ (struct
+ let option_name = "-ppt-fct"
+ let help = "Name of the function in which the property is defined"
+ let arg_name = ""
+ end)
+
+module Ppt_name =
+ EmptyString
+ (struct
+ let option_name = "-ppt-name"
+ let help = "Name of the property (assertion, ...)"
+ let arg_name = ""
+ end)
+
+module Ppt_line =
+ Zero
+ (struct
+ let option_name = "-ppt-line"
+ let help = "Line at which the property is defined"
+ let arg_name = ""
+ end)
+
+(* ************************************************************************** *)
+(* Searching the property according to plug-in's options *)
+(* ************************************************************************** *)
+
+exception Found of Property.t * int
+
+let search_assert kf =
+ try
+ Annotations.iter_all_code_annot
+ (fun stmt _ a ->
+ match a.annot_content with
+ | AAssert(_, p) ->
+ let line = Ppt_line.get () in
+ if (fst (p.loc)).Lexing.pos_lnum = line then
+ raise (Found(Property.ip_of_code_annot_single kf stmt a, line))
+ | _ -> ());
+ assert false
+ with Found(ppt, line) ->
+ ppt, line
+
+let is_predicate p line = (fst (p.ip_loc)).Lexing.pos_lnum = line
+
+let search_funspec_part iter convert kf =
+ try
+ Annotations.iter_behaviors
+ (fun _ bhv -> iter (fun _ a -> convert bhv a) kf bhv.b_name)
+ kf;
+ assert false
+ with Found(ppt, line) ->
+ ppt, line
+
+let search_ensures kf =
+ search_funspec_part
+ Annotations.iter_ensures
+ (fun bhv (_, p as a) ->
+ let line = Ppt_line.get () in
+ if is_predicate p line then
+ raise (Found (Property.ip_of_ensures kf Kglobal bhv a, line)) )
+ kf
+
+let search_requires kf =
+ search_funspec_part
+ Annotations.iter_requires
+ (fun bhv a ->
+ let line = Ppt_line.get () in
+ if is_predicate a line then
+ raise (Found (Property.ip_of_requires kf Kglobal bhv a, line)) )
+ kf
+
+let search kf = match Ppt_name.get () with
+ | "" | "Assertion" -> search_assert kf
+ | "Precondition" -> search_requires kf
+ | "Postcondition" -> search_ensures kf
+ | _ -> assert false
+
+(* ************************************************************************** *)
+(* Emitting status "invalid" for the property *)
+(* ************************************************************************** *)
+
+let emitter =
+ Emitter.create "E-ACSL" [ Emitter.Property_status ] ~correctness:[] ~tuning:[]
+
+let emit ppt line =
+ feedback "@[line %d:@ %a@ is@ invalid.@]" line Property.pretty ppt;
+ Property_status.emit emitter ~hyps:[] ppt Property_status.False_and_reachable
+
+(* ************************************************************************** *)
+(* Plug-in's main *)
+(* ************************************************************************** *)
+
+let main () =
+ let kf = Globals.Functions.find_by_name (Fct_name.get ()) in
+ let ppt, line = search kf in
+ emit ppt line
+
+let () = Db.Main.extend main
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 0c0a1ce71be..9c90716ad2c 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,12 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+-* E-ACSL [2013/05/30] Fixed -e-acsl-debug n, with n >= 2.
+
+###################################
+Plugin E-ACSL 0.2 Fluorine_20130401
+###################################
+
- E-ACSL [2013/01/09] New option -e-acsl-valid. By default, valid
annotation are not translated anymore.
-* E-ACSL [2013/01/09] Fix bug when translating a postcondition of a
diff --git a/src/plugins/e-acsl/gcc.sh b/src/plugins/e-acsl/gcc.sh
new file mode 100755
index 00000000000..7e367a3f252
--- /dev/null
+++ b/src/plugins/e-acsl/gcc.sh
@@ -0,0 +1,3 @@
+#!/bin/sh
+
+gcc -std=c99 -pedantic -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin -o $1.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_bittree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c $1 -lgmp && $1.out
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index 0e2312bb57b..a152d3128fa 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -160,10 +160,11 @@ let result_vi kf = match result_lhost kf with
(** {2 Handling the E-ACSL's C-libraries, part II} *)
(* ************************************************************************** *)
-(* TODO: convert -debug 2 into a new debugging category *)
let mk_debug_mmodel_stmt stmt =
- if Options.debug_atleast 2 then
- let debug = mk_call "__debug" [] in
+ if Options.debug_atleast 1
+ && Options.is_debug_key_enabled Options.dkey_analysis
+ then
+ let debug = mk_call "__e_acsl_memory_debug" [] in
Cil.mkStmt ~valid_sid:true (Block (Cil.mkBlock [ stmt; debug]))
else
stmt
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl.c b/src/plugins/e-acsl/share/e-acsl/e_acsl.c
index c08633e039d..5c7a153a4ba 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl.c
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl.c
@@ -2,7 +2,7 @@
/* */
/* This file is part of the Frama-C's E-ACSL plug-in. */
/* */
-/* Copyright (C) 2012 */
+/* Copyright (C) 2012-2013 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
index 4c70652ea7c..31dd8ed5695 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
@@ -1,3 +1,25 @@
+/**************************************************************************/
+/* */
+/* This file is part of the Frama-C's E-ACSL plug-in. */
+/* */
+/* Copyright (C) 2012-2013 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
#include <assert.h>
#include <errno.h>
#include <unistd.h>
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.h b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.h
index 81c724e589a..3738659e589 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.h
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.h
@@ -1,3 +1,25 @@
+/**************************************************************************/
+/* */
+/* This file is part of the Frama-C's E-ACSL plug-in. */
+/* */
+/* Copyright (C) 2012-2013 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
#ifndef E_ACSL_BITTREE
#define E_ACSL_BITTREE
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
index e2ec24d1079..50f5681edcf 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
@@ -1,3 +1,24 @@
+/**************************************************************************/
+/* */
+/* This file is part of the Frama-C's E-ACSL plug-in. */
+/* */
+/* Copyright (C) 2012-2013 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
#include <stdio.h>
#include <stdlib.h>
@@ -10,13 +31,12 @@
size_t __memory_size = 0;
/*unsigned cpt_store_block = 0;*/
-
const int nbr_bits_to_1[256] = {
0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
};
/*@ assigns \nothing;
- @ ensures \resul == __memory_size;
+ @ ensures \result == __memory_size;
@*/
size_t __get_memory_size(void) {
return __memory_size;
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
index 39eb7c215a2..ff4de942d7c 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
@@ -1,3 +1,24 @@
+/**************************************************************************/
+/* */
+/* This file is part of the Frama-C's E-ACSL plug-in. */
+/* */
+/* Copyright (C) 2012-2013 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
#ifndef E_ACSL_MMODEL
#define E_ACSL_MMODEL
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h
index 517ae2feba4..0dfb4359756 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h
@@ -1,3 +1,25 @@
+/**************************************************************************/
+/* */
+/* This file is part of the Frama-C's E-ACSL plug-in. */
+/* */
+/* Copyright (C) 2012-2013 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
#ifndef E_ACSL_MMODEL_API
#define E_ACSL_MMODEL_API
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle
index dfd6be32f6e..dda39b4964c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle
@@ -18,8 +18,8 @@
[value] using specification for function __full_init
tests/e-acsl-runtime/addrOf.i:12:[value] Assertion got status valid.
[value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function __delete_block
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 dfd6be32f6e..dda39b4964c 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
@@ -18,8 +18,8 @@
[value] using specification for function __full_init
tests/e-acsl-runtime/addrOf.i:12:[value] Assertion got status valid.
[value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function __delete_block
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
index 07fcdaf5d06..5411fb36704 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
@@ -20,8 +20,8 @@ tests/e-acsl-runtime/bts1304.i:23:[value] entering loop for the first time
[value] using specification for function __delete_block
tests/e-acsl-runtime/bts1304.i:25:[value] Assertion got status unknown.
[value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
[kernel] warning: Neither code nor specification for function __e_acsl_memory_clean, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle
index 07fcdaf5d06..5411fb36704 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle
@@ -20,8 +20,8 @@ tests/e-acsl-runtime/bts1304.i:23:[value] entering loop for the first time
[value] using specification for function __delete_block
tests/e-acsl-runtime/bts1304.i:25:[value] Assertion got status unknown.
[value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
[kernel] warning: Neither code nor specification for function __e_acsl_memory_clean, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
index 4e05beb5b82..26fdbdf56a1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
@@ -37,8 +37,8 @@ tests/e-acsl-runtime/bts1399.c:24:[value] Assertion got status valid.
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
FRAMAC_SHARE/libc/stdlib.h:142:[value] Function __e_acsl_free, behavior deallocation: precondition got status unknown.
FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
index 6b1be31fcb0..aa490e4d810 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
@@ -58,8 +58,8 @@ share/e-acsl/e_acsl_gmp.h:163:[value] Function __gmpz_tdiv_q: precondition got s
[value] using specification for function __gmpz_get_ui
share/e-acsl/e_acsl_gmp.h:194:[value] Function __gmpz_get_ui: precondition got status valid.
[value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
[value] using specification for function __gmpz_clear
share/e-acsl/e_acsl_gmp.h:114:[value] Function __gmpz_clear: precondition got status valid.
FRAMAC_SHARE/libc/stdlib.h:142:[value] Function __e_acsl_free, behavior deallocation: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle
index 367980e27e7..564a7b4632f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle
@@ -25,8 +25,8 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
[value] using specification for function __valid
tests/e-acsl-runtime/ghost.i:17:[value] Assertion got status valid.
[value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] using specification for function __delete_block
[kernel] warning: Neither code nor specification for function __e_acsl_memory_clean, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
index 92d0252727d..93d783ae148 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
@@ -38,8 +38,8 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
share/e-acsl/e_acsl_gmp.h:114:[value] Function __gmpz_clear: precondition got status valid.
tests/e-acsl-runtime/literal_string.i:25:[value] Assertion got status valid.
[value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
tests/e-acsl-runtime/literal_string.i:26:[value] Assertion got status valid.
[value] using specification for function __valid_read
tests/e-acsl-runtime/literal_string.i:27:[value] Assertion got status valid.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle
index 40f94b88cb3..5b920f33e5a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle
@@ -31,8 +31,8 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
tests/e-acsl-runtime/literal_string.i:25:[value] Assertion got status valid.
[value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
tests/e-acsl-runtime/literal_string.i:26:[value] Assertion got status valid.
tests/e-acsl-runtime/literal_string.i:27:[value] Assertion got status valid.
[value] using specification for function __valid
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
index 40a81d2213e..6928f226ea0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
@@ -29,8 +29,8 @@ FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior alloca
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid.
[value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
index 40a81d2213e..6928f226ea0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
@@ -29,8 +29,8 @@ FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior alloca
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid.
[value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
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 f859ef03dcb..f60e8f83e3e 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
@@ -19,8 +19,8 @@
[value] using specification for function __initialize
tests/e-acsl-runtime/ptr.i:13:[value] Assertion got status valid.
[value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
[value] using specification for function __valid_read
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
index 42d20c63188..65357e1cff8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
@@ -37,8 +37,8 @@ tests/e-acsl-runtime/ptr_init.c:28:[value] Assertion got status valid.
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
tests/e-acsl-runtime/ptr_init.c:29:[value] Assertion got status valid.
[value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
tests/e-acsl-runtime/ptr_init.c:19:[value] Assertion got status valid.
[kernel] warning: Neither code nor specification for function __e_acsl_memory_clean, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
index 42d20c63188..65357e1cff8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
@@ -37,8 +37,8 @@ tests/e-acsl-runtime/ptr_init.c:28:[value] Assertion got status valid.
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
tests/e-acsl-runtime/ptr_init.c:29:[value] Assertion got status valid.
[value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
tests/e-acsl-runtime/ptr_init.c:19:[value] Assertion got status valid.
[kernel] warning: Neither code nor specification for function __e_acsl_memory_clean, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
index c31f4f17a23..a611a506443 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
@@ -32,8 +32,8 @@ tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `\allocate' i
[value] using specification for function __full_init
tests/e-acsl-runtime/valid.c:35:[value] Assertion got status valid.
[value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
tests/e-acsl-runtime/valid.c:35:[kernel] warning: accessing uninitialized left-value: assert \initialized(&a);
tests/e-acsl-runtime/valid.c:35:[kernel] warning: completely indeterminate value in a.
tests/e-acsl-runtime/valid.c:35:[value] all evaluations are invalid for function call argument
@@ -49,7 +49,7 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/valid.c:37:[value] Assertion got status valid.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
tests/e-acsl-runtime/valid.c:37:[kernel] warning: accessing uninitialized left-value: assert \initialized(&b);
tests/e-acsl-runtime/valid.c:37:[kernel] warning: completely indeterminate value in b.
tests/e-acsl-runtime/valid.c:37:[value] all evaluations are invalid for function call argument
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
index c31f4f17a23..a611a506443 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
@@ -32,8 +32,8 @@ tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `\allocate' i
[value] using specification for function __full_init
tests/e-acsl-runtime/valid.c:35:[value] Assertion got status valid.
[value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
tests/e-acsl-runtime/valid.c:35:[kernel] warning: accessing uninitialized left-value: assert \initialized(&a);
tests/e-acsl-runtime/valid.c:35:[kernel] warning: completely indeterminate value in a.
tests/e-acsl-runtime/valid.c:35:[value] all evaluations are invalid for function call argument
@@ -49,7 +49,7 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/valid.c:37:[value] Assertion got status valid.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
tests/e-acsl-runtime/valid.c:37:[kernel] warning: accessing uninitialized left-value: assert \initialized(&b);
tests/e-acsl-runtime/valid.c:37:[kernel] warning: completely indeterminate value in b.
tests/e-acsl-runtime/valid.c:37:[value] all evaluations are invalid for function call argument
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
index ad833159dd4..56f011916a1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
@@ -29,8 +29,8 @@ tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `\alloc
[value] using specification for function __store_block
tests/e-acsl-runtime/valid_alias.c:12:[value] Assertion got status valid.
[value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
tests/e-acsl-runtime/valid_alias.c:12:[kernel] warning: accessing uninitialized left-value: assert \initialized(&a);
tests/e-acsl-runtime/valid_alias.c:12:[kernel] warning: completely indeterminate value in a.
tests/e-acsl-runtime/valid_alias.c:12:[value] all evaluations are invalid for function call argument
@@ -47,7 +47,7 @@ FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior alloca
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __initialize
tests/e-acsl-runtime/valid_alias.c:16:[value] Assertion got status valid.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
[value] using specification for function __valid
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
tests/e-acsl-runtime/valid_alias.c:17:[value] Assertion got status valid.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
index 132daabd9cc..6bbb1e532ed 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
@@ -29,8 +29,8 @@ tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `\alloc
[value] using specification for function __store_block
tests/e-acsl-runtime/valid_alias.c:12:[value] Assertion got status valid.
[value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
tests/e-acsl-runtime/valid_alias.c:12:[kernel] warning: accessing uninitialized left-value: assert \initialized(&a);
tests/e-acsl-runtime/valid_alias.c:12:[kernel] warning: completely indeterminate value in a.
tests/e-acsl-runtime/valid_alias.c:12:[value] all evaluations are invalid for function call argument
@@ -47,7 +47,7 @@ FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior alloca
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __initialize
tests/e-acsl-runtime/valid_alias.c:16:[value] Assertion got status valid.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
[value] using specification for function __valid
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
tests/e-acsl-runtime/valid_alias.c:17:[value] Assertion got status valid.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
index 92e4abd42c4..0ed09a24286 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
@@ -18,8 +18,8 @@
[value] using specification for function __store_block
[value] using specification for function __valid
[value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
[value] using specification for function __valid_read
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
index 92e4abd42c4..0ed09a24286 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
@@ -18,8 +18,8 @@
[value] using specification for function __store_block
[value] using specification for function __valid
[value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
[value] using specification for function __valid_read
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
index d5e6abb42d5..3a62b0c363a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
@@ -31,8 +31,8 @@ tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `\allocate'
[value] using specification for function __initialize
tests/e-acsl-runtime/vector.c:26:[value] Assertion got status valid.
[value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function __full_init
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
index ab6aa7e7c58..d1cf5ba1df8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
@@ -31,8 +31,8 @@ tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `\allocate'
[value] using specification for function __initialize
tests/e-acsl-runtime/vector.c:26:[value] Assertion got status valid.
[value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function __full_init
--
GitLab