Commit cde9885a authored by Julien Signoles's avatar Julien Signoles
Browse files

[E-ACSL] new option -e-acsl-valid. Valid annotations are not translated by default anymore.

[E-ACSL] code of e_acsl_assert put in e_acsl.c (no more in e_acsl.h)
parent f7a1cd74
......@@ -57,6 +57,7 @@ PLUGIN_CMO:= local_config \
error \
misc \
mpz \
init \
pre_analysis \
pre_visit \
env \
......
......@@ -15,6 +15,8 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
- 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
function where the init state is the same than the final
state (bts #!1300).
......
#!/bin/sh
gcc -std=c99 -pedantic -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $2 -o ./tests/e-acsl-runtime/result/gen_$1.out ./share/e-acsl/memory_model/e_acsl_bittree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/e-acsl-runtime/result/gen_$1.c -lgmp && ./tests/e-acsl-runtime/result/gen_$1.out
gcc -std=c99 -pedantic -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $2 -o ./tests/e-acsl-runtime/result/gen_$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 ./tests/e-acsl-runtime/result/gen_$1.c -lgmp && ./tests/e-acsl-runtime/result/gen_$1.out
......@@ -156,7 +156,7 @@ let predicate_to_exp =
Translate.predicate_to_exp
let add_e_acsl_library _files =
if Options.must_visit () then ignore (extend_ast ())
if Options.must_visit () || Options.Prepare.get () then ignore (extend_ast ())
let () = Cmdline.run_after_configuring_stage add_e_acsl_library
......
......@@ -55,6 +55,20 @@ module Project_name =
let arg_name = "prj"
end)
module Valid =
False
(struct
let option_name = "-e-acsl-valid"
let help = "translate annotation which have been proven valid"
end)
module Prepare =
False
(struct
let option_name = "-e-acsl-prepare"
let help = "prepare the AST to be directly usable by E-ACSL"
end)
module Gmp_only =
False
(struct
......
......@@ -26,6 +26,8 @@ include S (** implementation of Log.S for E-ACSL *)
module Check: Bool
module Run: Bool
module Valid: Bool
module Prepare: Bool
module Gmp_only: Bool
module Project_name: String
......
......@@ -29,6 +29,8 @@ open Cil_types
let fct_tbl: unit Kernel_function.Hashtbl.t = Kernel_function.Hashtbl.create 7
let is_generated_function kf = Kernel_function.Hashtbl.mem fct_tbl kf
let actions = Queue.create ()
module Global: sig
val add_logic_info: logic_info -> unit
val mem_logic_info: logic_info -> bool
......@@ -44,12 +46,48 @@ end
let reset () =
Kernel_function.Hashtbl.clear fct_tbl;
Global.reset ()
Global.reset ();
Queue.clear actions
(* ********************************************************************** *)
(* Duplicating property statuses *)
(* ********************************************************************** *)
let copy_ppt old_prj new_prj old_ppt new_ppt =
let module P = Property_status in
let selection = State_selection.of_list [ P.self; Emitter.self ] in
let emit s l =
Project.on ~selection new_prj
(fun s ->
let e = match l with [] -> assert false | e :: _ -> e in
(* Options.feedback "HERE %a --> %a (%a)" Property.pretty new_ppt
P.Emitted_status.pretty s Project.pretty new_prj;*)
if not e.P.logical_consequence then
let emitter = Emitter.Usable_emitter.get e.P.emitter in
(* Options.feedback "EMIT %a --> %a (%a)" Property.pretty new_ppt
P.Emitted_status.pretty s Project.pretty new_prj;*)
P.emit emitter ~hyps:e.P.properties new_ppt s)
s
in
let copy () =
match Project.on ~selection old_prj P.get old_ppt with
| P.Never_tried -> ()
| P.Best(s, l) -> emit s l
| P.Inconsistent i ->
emit P.True i.P.valid;
emit P.False_and_reachable i.P.invalid
in
if not (Options.Valid.get ()) then Queue.add copy actions
(* ********************************************************************** *)
(* Duplicating functions *)
(* ********************************************************************** *)
let dup_spec_status old_prj kf new_kf old_spec new_spec =
let old_ppts = Property.ip_of_spec kf Kglobal old_spec in
let new_ppts = Property.ip_of_spec new_kf Kglobal new_spec in
List.iter2 (copy_ppt old_prj (Project.current ())) old_ppts new_ppts
let dup_funspec tbl bhv spec =
(* Options.feedback "DUP SPEC %a" Cil.d_funspec spec;*)
let o = object
......@@ -148,25 +186,73 @@ let dup_fundec loc spec bhv kf vi new_vi =
sspec = new_spec },
return
let dup_global loc spec bhv kf vi new_vi =
let dup_global loc old_prj spec bhv kf vi new_vi =
(* Options.feedback "DUP GLOBAL %s" vi.vname;*)
let fundec, return = dup_fundec loc spec bhv kf vi new_vi in
let fct = Definition(fundec, loc) in
let spec = fundec.sspec in
let kf = { fundec = fct; return_stmt = Some return; spec = spec } in
Kernel_function.Hashtbl.add fct_tbl kf ();
Globals.Functions.register kf;
Globals.Functions.replace_by_definition spec fundec loc;
let new_spec = fundec.sspec in
let new_kf = { fundec = fct; return_stmt = Some return; spec = new_spec } in
Kernel_function.Hashtbl.add fct_tbl new_kf ();
Globals.Functions.register new_kf;
Globals.Functions.replace_by_definition new_spec fundec loc;
Annotations.register_funspec new_kf;
dup_spec_status old_prj kf new_kf spec new_spec;
GFun(fundec, loc)
(* ********************************************************************** *)
(* Visitor *)
(* ********************************************************************** *)
type position = Before_gmp | Gmp | After_gmp | Memory_model | Code
class dup_functions_visitor prj = object (self)
inherit Visitor.frama_c_copy prj
val fct_tbl = Cil_datatype.Varinfo.Hashtbl.create 7
val mutable before_memory_model = Before_gmp
val mutable libc_decls = []
method private before_memory_model = match before_memory_model with
| Before_gmp | Gmp | After_gmp -> true
| Memory_model | Code -> false
method private insert_libc l =
match libc_decls with
| [] -> l
| _ :: _ ->
let res = List.fold_left (fun acc g -> g :: acc) l libc_decls in
libc_decls <- [];
res
method private dup_libc g new_g =
if self#before_memory_model then begin
libc_decls <- new_g :: libc_decls;
[ g ]
end else
self#insert_libc [ g; new_g ]
method private next () =
match before_memory_model with
| Before_gmp -> ()
| Gmp -> before_memory_model <- After_gmp
| After_gmp -> ()
| Memory_model -> before_memory_model <- Code
| Code -> ()
method vcode_annot a =
Cil.JustCopyPost
(fun a' ->
let get_ppt kf stmt a = Property.ip_of_code_annot kf stmt a in
let kf = Extlib.the self#current_kf in
let stmt = Extlib.the self#current_stmt in
List.iter2
(fun p p' -> copy_ppt (Project.current ()) prj p p')
(get_ppt kf stmt a)
(get_ppt
(Cil.get_kernel_function self#behavior kf)
(Cil.get_stmt self#behavior stmt)
a');
a')
method vlogic_info_decl li =
Global.add_logic_info li;
......@@ -180,7 +266,7 @@ class dup_functions_visitor prj = object (self)
Cil.JustCopy
method vglob_aux = function
| GVarDecl(_, vi, loc) | GFun({ svar = vi }, loc)
| GVarDecl(_, vi, loc) | GFun({ svar = vi }, loc)
when Cil.isFunctionType vi.vtype
&& not (Misc.is_library_loc loc)
&& not (Cil.is_builtin vi)
......@@ -189,6 +275,7 @@ class dup_functions_visitor prj = object (self)
(Annotations.funspec ~populate:false
(Extlib.the self#current_kf)))
->
self#next ();
let name = "__e_acsl_" ^ vi.vname in
let new_vi = Project.on prj (Cil.makeGlobalVar name) vi.vtype in
Cil_datatype.Varinfo.Hashtbl.add fct_tbl vi new_vi;
......@@ -213,17 +300,36 @@ class dup_functions_visitor prj = object (self)
let spec = Annotations.funspec ~populate:false kf in
let vi_bhv = Cil.get_varinfo self#behavior vi in
let new_g =
Project.on prj (dup_global loc spec self#behavior kf vi_bhv)
Project.on prj
(dup_global loc (Project.current ()) spec self#behavior kf vi_bhv)
new_vi
in
[ g; new_g ]
self#dup_libc g new_g
| _ -> assert false)
| GVarDecl(_, vi, loc) | GFun({ svar = vi }, loc)
when Misc.is_library_loc loc || Cil.is_builtin vi
->
| GVarDecl(_, _, loc) | GFun(_, loc) when Misc.is_library_loc loc ->
(match before_memory_model with
| Before_gmp -> before_memory_model <- Gmp
| Gmp | Memory_model -> ()
| After_gmp -> before_memory_model <- Memory_model
| Code -> assert false);
Cil.JustCopy
| GVarDecl(_, vi, _) | GFun({ svar = vi }, _) when Cil.is_builtin vi ->
self#next ();
Cil.JustCopy
| _ ->
Cil.DoChildren
self#next ();
Cil.DoChildrenPost self#insert_libc
method vfile _ =
Cil.DoChildrenPost
(fun f ->
match libc_decls with
| [] -> f
| _ :: _ ->
(* in the rare case where there is no global tagged as [Code] in the
file *)
f.globals <- self#insert_libc f.globals;
f)
initializer reset ()
......@@ -236,6 +342,7 @@ let dup_functions () =
(new dup_functions_visitor)
in
Project.copy ~selection:(Plugin.get_selection ()) prj;
Queue.iter (fun f -> f ()) actions;
prj
(*
......
/**************************************************************************/
/* */
/* This file is part of the Frama-C's E-ACSL plug-in. */
/* */
/* Copyright (C) 2012 */
/* 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 "e_acsl.h"
#include "stdlib.h"
#include "stdio.h"
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line) {
if (! predicate) {
printf("%s failed at line %d.\nThe failing predicate is:\n%s.\n",
kind, line, pred_txt);
exit(1);
}
}
......@@ -27,10 +27,8 @@
#ifndef E_ACSL
#define E_ACSL
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line);
#include "stdlib.h"
#include "stdio.h"
/* #include "stdlib.h" */
/* #include "stdio.h" */
/*****************************/
/* Dedicated E-ACSL function */
......@@ -38,12 +36,13 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line);
/*@ requires predicate != 0;
@ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line) {
if (! predicate) {
printf("%s failed at line %d.\nThe failing predicate is:\n%s.\n",
kind, line, pred_txt);
exit(1);
}
}
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
__attribute__((FC_BUILTIN));/* { */
/* if (! predicate) { */
/* printf("%s failed at line %d.\nThe failing predicate is:\n%s.\n", */
/* kind, line, pred_txt); */
/* exit(1); */
/* } */
/* } */
#endif
......@@ -4,8 +4,6 @@
[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"
tests/e-acsl-runtime/addrOf.i:7:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......@@ -13,46 +11,13 @@ tests/e-acsl-runtime/addrOf.i:7:[e-acsl] warning: E-ACSL construct `assigns clau
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_stdout ∈ {{ NULL ; &S___fc_stdout }}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .__fc_mode; } ∈
[--..--]
[0].__fc_inode ∈ {{ NULL ; &S___fc_inode_0_S___fc_stdout }}
[1]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .__fc_mode; } ∈
[--..--]
[1].__fc_inode ∈ {{ NULL ; &S___fc_inode_1_S___fc_stdout }}
S___fc_inode_0_S___fc_stdout[0]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; } ∈
[--..--]
[0].__fc_real_data ∈
{{ NULL ;
&S___fc_real_data_0_S___fc_inode_0_S___fc_stdout }}
{[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; }; } ∈
[--..--]
[1].__fc_real_data ∈
{{ NULL ;
&S___fc_real_data_1_S___fc_inode_0_S___fc_stdout }}
[1].__fc_real_data_max_size ∈ [--..--]
S___fc_real_data_0_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_real_data_1_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_inode_1_S___fc_stdout[0]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; } ∈
[--..--]
[0].__fc_real_data ∈
{{ NULL ;
&S___fc_real_data_0_S___fc_inode_1_S___fc_stdout }}
{[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; }; } ∈
[--..--]
[1].__fc_real_data ∈
{{ NULL ;
&S___fc_real_data_1_S___fc_inode_1_S___fc_stdout }}
[1].__fc_real_data_max_size ∈ [--..--]
S___fc_real_data_0_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
S___fc_real_data_1_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
tests/e-acsl-runtime/addrOf.i:9:[value] Assertion got status valid.
./share/e-acsl/e_acsl.h:39:[value] Function e_acsl_assert: precondition got status valid.
[value] using specification for function e_acsl_assert
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status valid.
[value] using specification for function __clean
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function e_acsl_assert:
[value] Values at end of function main:
x ∈ {0}
__retres ∈ {0}
......@@ -4,8 +4,6 @@
[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"
tests/e-acsl-runtime/addrOf.i:7:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......@@ -13,46 +11,13 @@ tests/e-acsl-runtime/addrOf.i:7:[e-acsl] warning: E-ACSL construct `assigns clau
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_stdout ∈ {{ NULL ; &S___fc_stdout }}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .__fc_mode; } ∈
[--..--]
[0].__fc_inode ∈ {{ NULL ; &S___fc_inode_0_S___fc_stdout }}
[1]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .__fc_mode; } ∈
[--..--]
[1].__fc_inode ∈ {{ NULL ; &S___fc_inode_1_S___fc_stdout }}
S___fc_inode_0_S___fc_stdout[0]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; } ∈
[--..--]
[0].__fc_real_data ∈
{{ NULL ;
&S___fc_real_data_0_S___fc_inode_0_S___fc_stdout }}
{[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; }; } ∈
[--..--]
[1].__fc_real_data ∈
{{ NULL ;
&S___fc_real_data_1_S___fc_inode_0_S___fc_stdout }}
[1].__fc_real_data_max_size ∈ [--..--]
S___fc_real_data_0_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_real_data_1_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_inode_1_S___fc_stdout[0]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; } ∈
[--..--]
[0].__fc_real_data ∈
{{ NULL ;
&S___fc_real_data_0_S___fc_inode_1_S___fc_stdout }}
{[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; }; } ∈
[--..--]
[1].__fc_real_data ∈
{{ NULL ;
&S___fc_real_data_1_S___fc_inode_1_S___fc_stdout }}
[1].__fc_real_data_max_size ∈ [--..--]
S___fc_real_data_0_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
S___fc_real_data_1_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
tests/e-acsl-runtime/addrOf.i:9:[value] Assertion got status valid.
./share/e-acsl/e_acsl.h:39:[value] Function e_acsl_assert: precondition got status valid.
[value] using specification for function e_acsl_assert
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status valid.
[value] using specification for function __clean
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function e_acsl_assert:
[value] Values at end of function main:
x ∈ {0}
__retres ∈ {0}
......@@ -4,8 +4,6 @@
[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"
tests/e-acsl-runtime/arith.i:8:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......@@ -13,39 +11,6 @@ tests/e-acsl-runtime/arith.i:8:[e-acsl] warning: E-ACSL construct `assigns claus
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_stdout ∈ {{ NULL ; &S___fc_stdout }}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .__fc_mode; } ∈
[--..--]
[0].__fc_inode ∈ {{ NULL ; &S___fc_inode_0_S___fc_stdout }}
[1]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .__fc_mode; } ∈
[--..--]
[1].__fc_inode ∈ {{ NULL ; &S___fc_inode_1_S___fc_stdout }}
S___fc_inode_0_S___fc_stdout[0]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; } ∈
[--..--]
[0].__fc_real_data ∈
{{ NULL ;
&S___fc_real_data_0_S___fc_inode_0_S___fc_stdout }}
{[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; }; } ∈
[--..--]
[1].__fc_real_data ∈
{{ NULL ;
&S___fc_real_data_1_S___fc_inode_0_S___fc_stdout }}
[1].__fc_real_data_max_size ∈ [--..--]
S___fc_real_data_0_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_real_data_1_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_inode_1_S___fc_stdout[0]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; } ∈
[--..--]
[0].__fc_real_data ∈
{{ NULL ;
&S___fc_real_data_0_S___fc_inode_1_S___fc_stdout }}
{[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; }; } ∈
[--..--]
[1].__fc_real_data ∈
{{ NULL ;
&S___fc_real_data_1_S___fc_inode_1_S___fc_stdout }}
[1].__fc_real_data_max_size ∈ [--..--]
S___fc_real_data_0_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
S___fc_real_data_1_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
tests/e-acsl-runtime/arith.i:12:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_si
./share/e-acsl/e_acsl_gmp.h:61:[value] Function __gmpz_init_set_si: precondition got status valid.
......@@ -60,7 +25,8 @@ tests/e-acsl-runtime/arith.i:12:[value] Assertion got status valid.
[value] using specification for function __gmpz_cmp
./share/e-acsl/e_acsl_gmp.h:115:[value] Function __gmpz_cmp: precondition got status valid.
./share/e-acsl/e_acsl_gmp.h:116:[value] Function __gmpz_cmp: precondition got status valid.
./share/e-acsl/e_acsl.h:39:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function e_acsl_assert
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
./share/e-acsl/e_acsl_gmp.h:105:[value] Function __gmpz_clear: precondition got status valid.
tests/e-acsl-runtime/arith.i:13:[value] Assertion got status valid.
......@@ -111,7 +77,6 @@ tests/e-acsl-runtime/arith.i:33:[value] Assertion got status valid.
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function e_acsl_assert:
[value] Values at end of function main:
x ∈ {-3}
y ∈ {2}
......
......@@ -4,8 +4,6 @@
[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"
tests/e-acsl-runtime/arith.i:8:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......@@ -13,41 +11,9 @@ tests/e-acsl-runtime/arith.i:8:[e-acsl] warning: E-ACSL construct `assigns claus
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_stdout ∈ {{ NULL ; &S___fc_stdout }}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .__fc_mode; } ∈
[--..--]
[0].__fc_inode ∈ {{ NULL ; &S___fc_inode_0_S___fc_stdout }}
[1]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .__fc_mode; } ∈
[--..--]
[1].__fc_inode ∈ {{ NULL ; &S___fc_inode_1_S___fc_stdout }}
S___fc_inode_0_S___fc_stdout[0]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; } ∈
[--..--]
[0].__fc_real_data ∈
{{ NULL ;
&S___fc_real_data_0_S___fc_inode_0_S___fc_stdout }}
{[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; }; } ∈
[--..--]
[1].__fc_real_data ∈
{{ NULL ;
&S___fc_real_data_1_S___fc_inode_0_S___fc_stdout }}
[1].__fc_real_data_max_size ∈ [--..--]
S___fc_real_data_0_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_real_data_1_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_inode_1_S___fc_stdout[0]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; } ∈
[--..--]
[0].__fc_real_data ∈
{{ NULL ;
&S___fc_real_data_0_S___fc_inode_1_S___fc_stdout }}
{[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; }; } ∈
[--..--]
[1].__fc_real_data ∈
{{ NULL ;
&S___fc_real_data_1_S___fc_inode_1_S___fc_stdout }}
[1].__fc_real_data_max_size ∈ [--..--]
S___fc_real_data_0_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
S___fc_real_data_1_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
tests/e-acsl-runtime/arith.i:12:[value] Assertion got status valid.
./share/e-acsl/e_acsl.h:39:[value] Function e_acsl_assert: precondition got status valid.
[value] using specification for function e_acsl_assert
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status valid.
tests/e-acsl-runtime/arith.i:13:[value] Assertion got status valid.
tests/e-acsl-runtime/arith.i:14:[value] Assertion got status valid.
tests/e-acsl-runtime/arith.i:16:[value] Assertion got status valid.
......@@ -69,7 +35,6 @@ tests/e-acsl-runtime/arith.i:33:[value] Assertion got status valid.
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function e_acsl_assert:
[value] Values at end of function main:
x ∈ {-3}
y ∈ {2}
......
......@@ -4,8 +4,6 @@
[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"
tests/e-acsl-runtime/array.i:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......@@ -13,51 +11,18 @@ tests/e-acsl-runtime/array.i:10:[e-acsl] warning: E-ACSL construct `assigns clau
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_stdout ∈ {{ NULL ; &S___fc_stdout }}
T1[0..2] ∈ {0}
T2[0..3] ∈ {0}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .__fc_mode; } ∈
[--..--]
[0].__fc_inode ∈ {{ NULL ; &S___fc_inode_0_S___fc_stdout }}
[1]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .__fc_mode; } ∈
[--..--]
[1].__fc_inode ∈ {{ NULL ; &S___fc_inode_1_S___fc_stdout }}
S___fc_inode_0_S___fc_stdout[0]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; } ∈
[--..--]
[0].__fc_real_data ∈
{{ NULL ;
&S___fc_real_data_0_S___fc_inode_0_S___fc_stdout }}
{[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; }; } ∈