[E-ACSL] add demo

[E-ACSL] fixed bug in debug mode
[E-ACSL] add missing headers

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 #

src/plugins/e-acsl/TODO

@@ -5,27 +5,28 @@
 - [Bernard] avoir une fonction e_acsl_trace_behavior(char *bhv_name) {}
    appeler ds 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 initialise mais non utilise en prsence de \at
-  (voir test result.i, cas -e-acsl-gmp-only)
+- Gestion du mode -lib-entry
 - gnrer les delete des globals dans une fonction spare, 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 initialise mais non utilise en prsence de \at
+  (voir test result.i, cas -e-acsl-gmp-only)
 - comparaisons qui aboutissent  du C incorrect
   ==> comparaison de chanes litrales
    (voir tests other_constants.i et comparison.i)
@@ -57,21 +62,17 @@
 - incorrect d'utiliser Pre, Post, Here, Old dans stmt contract 
   (mme problme que Jessie: cf. BTS #72)
   (voir aussi result.i et ./at_stmt_contract.i)
-- interprtation 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)
+- interprtation 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

src/plugins/e-acsl/demo/TODO

+les TODO et assert false dans script.ml

src/plugins/e-acsl/demo/alone.sh

+#! /bin/sh
+frama-c demo.c -e-acsl -then-on e-acsl -print -ocode res_demo.c

src/plugins/e-acsl/demo/clean.sh

+#!/bin/bash
+
+clean
+rm -f demo.sav demo script frama_c_journal.ml res_demo.c
+./compile.sh

src/plugins/e-acsl/demo/compile.sh

+#!/bin/sh
+ocamlopt.opt -shared -o ./Script.cmxs -w Ly -warn-error A -I /usr/local/lib/frama-c -I . script.ml

src/plugins/e-acsl/demo/demo.c

+/*@ 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; */
+}

src/plugins/e-acsl/demo/demo.sh

+#! /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

src/plugins/e-acsl/demo/load.sh

+#!/bin/bash
+
+frama-c-gui -load demo.sav

src/plugins/e-acsl/demo/my_e_acsl.c

+#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);
+      }
+    }
+  }
+}

src/plugins/e-acsl/demo/pow.c

+#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;
+}

src/plugins/e-acsl/demo/run_demo.sh

+#! /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

src/plugins/e-acsl/demo/run_script.sh

+#! /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

src/plugins/e-acsl/demo/script.ml

+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

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

src/plugins/e-acsl/gcc.sh

+#!/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

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

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)                                                  */
 /*                                                                        */

src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c

+/**************************************************************************/
+/*                                                                        */
+/*  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>

src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.h

+/**************************************************************************/
+/*                                                                        */
+/*  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