diff --git a/basic-cwe-examples/.frama-c/GNUmakefile b/basic-cwe-examples/.frama-c/GNUmakefile
index b6b51aef26173031ef233d7236592cb99e023884..787ebe0b5a7e38a61a0ea15eb62d940017730c32 100644
--- a/basic-cwe-examples/.frama-c/GNUmakefile
+++ b/basic-cwe-examples/.frama-c/GNUmakefile
@@ -45,10 +45,10 @@ cwe416-precise.parse: ../cwe416.c
 cwe787-precise.parse: ../cwe787.c
 
 cwe20-precise.eva:  EVAFLAGS +=
-cwe119-precise.eva: EVAFLAGS += -eva-precision 1
-cwe190-precise.eva: EVAFLAGS += -warn-unsigned-overflow -eva-no-alloc-returns-null
-cwe416-precise.eva: EVAFLAGS += -eva-precision 1
-cwe787-precise.eva: EVAFLAGS += -eva-precision 2 -eva-no-alloc-returns-null
+cwe119-precise.eva: EVAFLAGS +=
+cwe190-precise.eva: EVAFLAGS += -warn-unsigned-overflow
+cwe416-precise.eva: EVAFLAGS +=
+cwe787-precise.eva: EVAFLAGS += -eva-precision 2
 
 ### Epilogue. Do not modify this block. #######################################
 include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk
diff --git a/basic-cwe-examples/.frama-c/cwe119-precise.eva/alarms.csv b/basic-cwe-examples/.frama-c/cwe119-precise.eva/alarms.csv
index 8fb375b87e9f1f54fa31aa22109caa8c635cba64..2d595fe025c8a4b55649753742ba43095f504748 100644
--- a/basic-cwe-examples/.frama-c/cwe119-precise.eva/alarms.csv
+++ b/basic-cwe-examples/.frama-c/cwe119-precise.eva/alarms.csv
@@ -1,3 +1,5 @@
 directory	file	line	function	property kind	status	property
-.	cwe119.c	62	host_lookup	precondition of strcpy	Unknown	room_string: \valid(dest + (0 .. strlen(src)))
-FRAMAC_SHARE/libc	string.h	352	strcpy	precondition	Unknown	room_string: \valid(dest + (0 .. strlen(src)))
+.	cwe119.c	28	my_strcmp	mem_access	Unknown	\valid_read(s1 + i)
+.	cwe119.c	28	my_strcmp	mem_access	Unknown	\valid_read(s2 + i)
+.	cwe119.c	65	host_lookup	precondition of strcpy	Invalid or unreachable	room_string: \valid(dest + (0 .. strlen(src)))
+FRAMAC_SHARE/libc	string.h	352	strcpy	precondition	Invalid or unreachable	room_string: \valid(dest + (0 .. strlen(src)))
diff --git a/basic-cwe-examples/.frama-c/cwe119-precise.eva/metrics.log b/basic-cwe-examples/.frama-c/cwe119-precise.eva/metrics.log
index 8d097e6b8adbbfe75d4b1325b13755c4816c86fa..8883390a7e1506f4b1eafd01a26aaf1ceb11f3f4 100644
--- a/basic-cwe-examples/.frama-c/cwe119-precise.eva/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe119-precise.eva/metrics.log
@@ -1,14 +1,15 @@
 [metrics] Eva coverage statistics
 =======================
-Syntactically reachable functions = 6 (out of 6)
-Semantically reached functions = 6
+Syntactically reachable functions = 7 (out of 7)
+Semantically reached functions = 7
 Coverage estimation = 100.0%
 [metrics] Statements analyzed by Eva
 --------------------------
-47 stmts in analyzed functions, 45 stmts analyzed (95.7%)
-host_lookup: 7 stmts out of 7 (100.0%)
-my_gethostbyaddr: 5 stmts out of 5 (100.0%)
+54 stmts in analyzed functions, 48 stmts analyzed (88.9%)
 my_inet_addr: 10 stmts out of 10 (100.0%)
 my_strcmp: 12 stmts out of 12 (100.0%)
+nonzero_uint32_t: 9 stmts out of 9 (100.0%)
 validate_addr_form: 7 stmts out of 7 (100.0%)
-main: 4 stmts out of 6 (66.7%)
+host_lookup: 4 stmts out of 5 (80.0%)
+my_gethostbyaddr: 4 stmts out of 5 (80.0%)
+main: 2 stmts out of 6 (33.3%)
diff --git a/basic-cwe-examples/.frama-c/cwe119-precise.eva/nonterm.log b/basic-cwe-examples/.frama-c/cwe119-precise.eva/nonterm.log
index 1f3822301d4aee0b9db2f49fd08d7bcffeb0e5b0..a6681f2652fd3b848bf5972b880d71c19ba1d6b7 100644
--- a/basic-cwe-examples/.frama-c/cwe119-precise.eva/nonterm.log
+++ b/basic-cwe-examples/.frama-c/cwe119-precise.eva/nonterm.log
@@ -1,3 +1,3 @@
-cwe119.c:62:[nonterm] warning: non-terminating function call
-stack: host_lookup :: cwe119.c:69 <- main
-cwe119.c:70:[nonterm] warning: unreachable return
+cwe119.c:65:[nonterm] warning: non-terminating function call
+stack: host_lookup :: cwe119.c:70 <- main
+cwe119.c:73:[nonterm] warning: unreachable return
diff --git a/basic-cwe-examples/.frama-c/cwe119-precise.parse/framac.ast b/basic-cwe-examples/.frama-c/cwe119-precise.parse/framac.ast
index a9cac3fad3c962586fc468ef7d5bfd7d9b4da4ec..9df9879f06110f0358b2f8a760a003be5d8659db 100644
--- a/basic-cwe-examples/.frama-c/cwe119-precise.parse/framac.ast
+++ b/basic-cwe-examples/.frama-c/cwe119-precise.parse/framac.ast
@@ -1,5 +1,4 @@
 /* Generated by Frama-C */
-#include "__fc_builtin.h"
 #include "errno.h"
 #include "inttypes.h"
 #include "netdb.h"
@@ -14,6 +13,22 @@
 #include "strings.h"
 #include "sys/socket.h"
 #include "sys/uio.h"
+uint32_t volatile _rand;
+uint32_t nonzero_uint32_t(void)
+{
+  uint32_t __retres;
+  uint32_t r = _rand;
+  if (! r) {
+    __retres = 1U;
+    goto return_label;
+  }
+  else {
+    __retres = r;
+    goto return_label;
+  }
+  return_label: return __retres;
+}
+
 /*@ requires valid_read_string(format);
     assigns \result, stream->__fc_FILE_data;
     assigns \result
@@ -66,9 +81,9 @@ static in_addr_t my_inet_addr(char const *cp)
     goto return_label;
   }
   else {
-    int tmp;
-    tmp = Frama_C_nondet(1,(int)4294967295U);
-    __retres = (unsigned int)tmp;
+    in_addr_t tmp;
+    tmp = nonzero_uint32_t();
+    __retres = tmp;
     goto return_label;
   }
   return_label: return __retres;
@@ -88,13 +103,11 @@ static struct hostent *my_gethostbyaddr(void const *addr, socklen_t len,
 void host_lookup(char *user_supplied_addr)
 {
   struct hostent *hp;
-  in_addr_t *addr;
+  in_addr_t addr;
   char hostname[64];
-  in_addr_t tmp;
   validate_addr_form(user_supplied_addr);
-  tmp = my_inet_addr((char const *)user_supplied_addr);
-  addr = (in_addr_t *)tmp;
-  hp = my_gethostbyaddr((void const *)addr,sizeof(struct in_addr),2);
+  addr = my_inet_addr((char const *)user_supplied_addr);
+  hp = my_gethostbyaddr((void const *)(& addr),sizeof(struct in_addr),2);
   strcpy(hostname,(char const *)hp->h_name);
   return;
 }
diff --git a/basic-cwe-examples/.frama-c/cwe119-precise.parse/metrics.log b/basic-cwe-examples/.frama-c/cwe119-precise.parse/metrics.log
index d20479d450cd42999f695ab92ce3a56a53506f87..06e1d8be49be7d74fb74ac753ea72544b69fef60 100644
--- a/basic-cwe-examples/.frama-c/cwe119-precise.parse/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe119-precise.parse/metrics.log
@@ -1,7 +1,8 @@
-[metrics] Defined functions (6)
+[metrics] Defined functions (7)
 =====================
  host_lookup (2 calls); main (0 call); my_gethostbyaddr (1 call);
- my_inet_addr (1 call); my_strcmp (1 call); validate_addr_form (1 call); 
+ my_inet_addr (1 call); my_strcmp (1 call); nonzero_uint32_t (1 call);
+ validate_addr_form (1 call); 
 
 Specified-only functions (0)
 ============================
@@ -21,15 +22,15 @@ Potential entry points (1)
 
 Global metrics
 ============== 
-Sloc = 47
-Decision point = 5
-Global variables = 1
-If = 5
+Sloc = 54
+Decision point = 6
+Global variables = 2
+If = 6
 Loop = 1
-Goto = 3
-Assignment = 19
-Exit point = 6
-Function = 6
+Goto = 5
+Assignment = 21
+Exit point = 7
+Function = 7
 Function call = 12
 Pointer dereferencing = 6
-Cyclomatic complexity = 11
+Cyclomatic complexity = 13
diff --git a/basic-cwe-examples/.frama-c/cwe119.eva/alarms.csv b/basic-cwe-examples/.frama-c/cwe119.eva/alarms.csv
index 692590ced2fccd77a2237fea063806509b8cc2e8..2d595fe025c8a4b55649753742ba43095f504748 100644
--- a/basic-cwe-examples/.frama-c/cwe119.eva/alarms.csv
+++ b/basic-cwe-examples/.frama-c/cwe119.eva/alarms.csv
@@ -1,5 +1,5 @@
 directory	file	line	function	property kind	status	property
-.	cwe119.c	25	my_strcmp	mem_access	Unknown	\valid_read(s1 + i)
-.	cwe119.c	25	my_strcmp	mem_access	Unknown	\valid_read(s2 + i)
-.	cwe119.c	62	host_lookup	precondition of strcpy	Unknown	room_string: \valid(dest + (0 .. strlen(src)))
-FRAMAC_SHARE/libc	string.h	352	strcpy	precondition	Unknown	room_string: \valid(dest + (0 .. strlen(src)))
+.	cwe119.c	28	my_strcmp	mem_access	Unknown	\valid_read(s1 + i)
+.	cwe119.c	28	my_strcmp	mem_access	Unknown	\valid_read(s2 + i)
+.	cwe119.c	65	host_lookup	precondition of strcpy	Invalid or unreachable	room_string: \valid(dest + (0 .. strlen(src)))
+FRAMAC_SHARE/libc	string.h	352	strcpy	precondition	Invalid or unreachable	room_string: \valid(dest + (0 .. strlen(src)))
diff --git a/basic-cwe-examples/.frama-c/cwe119.eva/metrics.log b/basic-cwe-examples/.frama-c/cwe119.eva/metrics.log
index a66ce1aca2090ede60da37f08c407e59a7bcc004..8883390a7e1506f4b1eafd01a26aaf1ceb11f3f4 100644
--- a/basic-cwe-examples/.frama-c/cwe119.eva/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe119.eva/metrics.log
@@ -1,14 +1,15 @@
 [metrics] Eva coverage statistics
 =======================
-Syntactically reachable functions = 6 (out of 6)
-Semantically reached functions = 6
+Syntactically reachable functions = 7 (out of 7)
+Semantically reached functions = 7
 Coverage estimation = 100.0%
 [metrics] Statements analyzed by Eva
 --------------------------
-47 stmts in analyzed functions, 47 stmts analyzed (100.0%)
-host_lookup: 7 stmts out of 7 (100.0%)
-main: 6 stmts out of 6 (100.0%)
-my_gethostbyaddr: 5 stmts out of 5 (100.0%)
+54 stmts in analyzed functions, 48 stmts analyzed (88.9%)
 my_inet_addr: 10 stmts out of 10 (100.0%)
 my_strcmp: 12 stmts out of 12 (100.0%)
+nonzero_uint32_t: 9 stmts out of 9 (100.0%)
 validate_addr_form: 7 stmts out of 7 (100.0%)
+host_lookup: 4 stmts out of 5 (80.0%)
+my_gethostbyaddr: 4 stmts out of 5 (80.0%)
+main: 2 stmts out of 6 (33.3%)
diff --git a/basic-cwe-examples/.frama-c/cwe119.eva/nonterm.log b/basic-cwe-examples/.frama-c/cwe119.eva/nonterm.log
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..a6681f2652fd3b848bf5972b880d71c19ba1d6b7 100644
--- a/basic-cwe-examples/.frama-c/cwe119.eva/nonterm.log
+++ b/basic-cwe-examples/.frama-c/cwe119.eva/nonterm.log
@@ -0,0 +1,3 @@
+cwe119.c:65:[nonterm] warning: non-terminating function call
+stack: host_lookup :: cwe119.c:70 <- main
+cwe119.c:73:[nonterm] warning: unreachable return
diff --git a/basic-cwe-examples/.frama-c/cwe119.parse/framac.ast b/basic-cwe-examples/.frama-c/cwe119.parse/framac.ast
index a9cac3fad3c962586fc468ef7d5bfd7d9b4da4ec..9df9879f06110f0358b2f8a760a003be5d8659db 100644
--- a/basic-cwe-examples/.frama-c/cwe119.parse/framac.ast
+++ b/basic-cwe-examples/.frama-c/cwe119.parse/framac.ast
@@ -1,5 +1,4 @@
 /* Generated by Frama-C */
-#include "__fc_builtin.h"
 #include "errno.h"
 #include "inttypes.h"
 #include "netdb.h"
@@ -14,6 +13,22 @@
 #include "strings.h"
 #include "sys/socket.h"
 #include "sys/uio.h"
+uint32_t volatile _rand;
+uint32_t nonzero_uint32_t(void)
+{
+  uint32_t __retres;
+  uint32_t r = _rand;
+  if (! r) {
+    __retres = 1U;
+    goto return_label;
+  }
+  else {
+    __retres = r;
+    goto return_label;
+  }
+  return_label: return __retres;
+}
+
 /*@ requires valid_read_string(format);
     assigns \result, stream->__fc_FILE_data;
     assigns \result
@@ -66,9 +81,9 @@ static in_addr_t my_inet_addr(char const *cp)
     goto return_label;
   }
   else {
-    int tmp;
-    tmp = Frama_C_nondet(1,(int)4294967295U);
-    __retres = (unsigned int)tmp;
+    in_addr_t tmp;
+    tmp = nonzero_uint32_t();
+    __retres = tmp;
     goto return_label;
   }
   return_label: return __retres;
@@ -88,13 +103,11 @@ static struct hostent *my_gethostbyaddr(void const *addr, socklen_t len,
 void host_lookup(char *user_supplied_addr)
 {
   struct hostent *hp;
-  in_addr_t *addr;
+  in_addr_t addr;
   char hostname[64];
-  in_addr_t tmp;
   validate_addr_form(user_supplied_addr);
-  tmp = my_inet_addr((char const *)user_supplied_addr);
-  addr = (in_addr_t *)tmp;
-  hp = my_gethostbyaddr((void const *)addr,sizeof(struct in_addr),2);
+  addr = my_inet_addr((char const *)user_supplied_addr);
+  hp = my_gethostbyaddr((void const *)(& addr),sizeof(struct in_addr),2);
   strcpy(hostname,(char const *)hp->h_name);
   return;
 }
diff --git a/basic-cwe-examples/.frama-c/cwe119.parse/metrics.log b/basic-cwe-examples/.frama-c/cwe119.parse/metrics.log
index d20479d450cd42999f695ab92ce3a56a53506f87..06e1d8be49be7d74fb74ac753ea72544b69fef60 100644
--- a/basic-cwe-examples/.frama-c/cwe119.parse/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe119.parse/metrics.log
@@ -1,7 +1,8 @@
-[metrics] Defined functions (6)
+[metrics] Defined functions (7)
 =====================
  host_lookup (2 calls); main (0 call); my_gethostbyaddr (1 call);
- my_inet_addr (1 call); my_strcmp (1 call); validate_addr_form (1 call); 
+ my_inet_addr (1 call); my_strcmp (1 call); nonzero_uint32_t (1 call);
+ validate_addr_form (1 call); 
 
 Specified-only functions (0)
 ============================
@@ -21,15 +22,15 @@ Potential entry points (1)
 
 Global metrics
 ============== 
-Sloc = 47
-Decision point = 5
-Global variables = 1
-If = 5
+Sloc = 54
+Decision point = 6
+Global variables = 2
+If = 6
 Loop = 1
-Goto = 3
-Assignment = 19
-Exit point = 6
-Function = 6
+Goto = 5
+Assignment = 21
+Exit point = 7
+Function = 7
 Function call = 12
 Pointer dereferencing = 6
-Cyclomatic complexity = 11
+Cyclomatic complexity = 13
diff --git a/basic-cwe-examples/.frama-c/cwe190-precise.eva/alarms.csv b/basic-cwe-examples/.frama-c/cwe190-precise.eva/alarms.csv
index d7352a280e4970eb11a0c15efbda9ce22bd807aa..7ef8d232e0063d0c495bcc04c52a6c0fdee962fc 100644
--- a/basic-cwe-examples/.frama-c/cwe190-precise.eva/alarms.csv
+++ b/basic-cwe-examples/.frama-c/cwe190-precise.eva/alarms.csv
@@ -1,2 +1,2 @@
 directory	file	line	function	property kind	status	property
-.	cwe190.c	38	main	unsigned_overflow	Invalid or unreachable	(unsigned int)nresp * sizeof(char *) ≤ 4294967295
+.	cwe190.c	42	main	unsigned_overflow	Invalid or unreachable	(unsigned int)nresp * sizeof(char *) ≤ 4294967295
diff --git a/basic-cwe-examples/.frama-c/cwe190-precise.eva/metrics.log b/basic-cwe-examples/.frama-c/cwe190-precise.eva/metrics.log
index 869047fdc603d28c5aa5308c74d89524d73bda2b..4da1ec297fb7c301fdfe3c2e0719cc452cb69f0e 100644
--- a/basic-cwe-examples/.frama-c/cwe190-precise.eva/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe190-precise.eva/metrics.log
@@ -1,12 +1,13 @@
 [metrics] Eva coverage statistics
 =======================
-Syntactically reachable functions = 4 (out of 4)
-Semantically reached functions = 4
+Syntactically reachable functions = 5 (out of 5)
+Semantically reached functions = 5
 Coverage estimation = 100.0%
 [metrics] Statements analyzed by Eva
 --------------------------
-30 stmts in analyzed functions, 20 stmts analyzed (66.7%)
-packet_get_int_ok: 2 stmts out of 2 (100.0%)
-packet_get_int_problem: 2 stmts out of 2 (100.0%)
+41 stmts in analyzed functions, 31 stmts analyzed (75.6%)
+packet_get_int_ok: 5 stmts out of 5 (100.0%)
+packet_get_int_problem: 5 stmts out of 5 (100.0%)
 packet_get_string: 2 stmts out of 2 (100.0%)
-main: 14 stmts out of 24 (58.3%)
+random_int: 1 stmts out of 1 (100.0%)
+main: 18 stmts out of 28 (64.3%)
diff --git a/basic-cwe-examples/.frama-c/cwe190-precise.eva/nonterm.log b/basic-cwe-examples/.frama-c/cwe190-precise.eva/nonterm.log
index a2c084e5d2221eb3ac11456b567471d929410647..e238d5be464fd4bde899ea54a5297ba1e8fec236 100644
--- a/basic-cwe-examples/.frama-c/cwe190-precise.eva/nonterm.log
+++ b/basic-cwe-examples/.frama-c/cwe190-precise.eva/nonterm.log
@@ -1,2 +1,2 @@
-cwe190.c:38:[nonterm] warning: non-terminating function call
+cwe190.c:42:[nonterm] warning: non-terminating function call
 stack: main
diff --git a/basic-cwe-examples/.frama-c/cwe190-precise.parse/framac.ast b/basic-cwe-examples/.frama-c/cwe190-precise.parse/framac.ast
index c0423908914c9a7eb7ecd3ef8f06e7336fa9fbc0..9ed5602e800862fd22b0d3ffaef5595cba001491 100644
--- a/basic-cwe-examples/.frama-c/cwe190-precise.parse/framac.ast
+++ b/basic-cwe-examples/.frama-c/cwe190-precise.parse/framac.ast
@@ -1,17 +1,27 @@
 /* Generated by Frama-C */
 #include "stdlib.h"
+int volatile _rand;
+int random_int(void)
+{
+  return _rand;
+}
+
 int packet_get_int_ok(void)
 {
-  int __retres;
-  __retres = 123456;
-  return __retres;
+  int tmp_0;
+  int tmp;
+  tmp = random_int();
+  if (tmp) tmp_0 = 0; else tmp_0 = 123456;
+  return tmp_0;
 }
 
 int packet_get_int_problem(void)
 {
-  int __retres;
-  __retres = 1073741824;
-  return __retres;
+  int tmp_0;
+  int tmp;
+  tmp = random_int();
+  if (tmp) tmp_0 = 1073741824; else tmp_0 = 0;
+  return tmp_0;
 }
 
 char *packet_get_string(char const *s)
@@ -28,6 +38,7 @@ int main(void)
   int nresp = packet_get_int_ok();
   if (nresp > 0) {
     response = (char **)malloc((unsigned int)nresp * sizeof(char *));
+    if (! response) exit(1);
     {
       int i = 0;
       while (i < nresp) {
@@ -35,11 +46,12 @@ int main(void)
         i ++;
       }
     }
+    free((void *)response);
   }
-  free((void *)response);
   nresp = packet_get_int_problem();
   if (nresp > 0) {
     response = (char **)malloc((unsigned int)nresp * sizeof(char *));
+    if (! response) exit(1);
     {
       int i_0 = 0;
       while (i_0 < nresp) {
@@ -47,8 +59,8 @@ int main(void)
         i_0 ++;
       }
     }
+    free((void *)response);
   }
-  free((void *)response);
   __retres = 0;
   return __retres;
 }
diff --git a/basic-cwe-examples/.frama-c/cwe190-precise.parse/metrics.log b/basic-cwe-examples/.frama-c/cwe190-precise.parse/metrics.log
index 209600bca2c7e1edb8152cee2f378db7eb7bb346..94c58dcd1ea028aaca899819eb25a539103ff441 100644
--- a/basic-cwe-examples/.frama-c/cwe190-precise.parse/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe190-precise.parse/metrics.log
@@ -1,7 +1,7 @@
-[metrics] Defined functions (4)
+[metrics] Defined functions (5)
 =====================
  main (0 call); packet_get_int_ok (1 call); packet_get_int_problem (1 call);
- packet_get_string (2 calls); 
+ packet_get_string (2 calls); random_int (2 calls); 
 
 Specified-only functions (0)
 ============================
@@ -21,15 +21,15 @@ Potential entry points (1)
 
 Global metrics
 ============== 
-Sloc = 30
-Decision point = 4
-Global variables = 0
-If = 4
+Sloc = 41
+Decision point = 8
+Global variables = 1
+If = 8
 Loop = 2
 Goto = 0
-Assignment = 14
-Exit point = 4
-Function = 4
-Function call = 8
+Assignment = 18
+Exit point = 5
+Function = 5
+Function call = 12
 Pointer dereferencing = 2
-Cyclomatic complexity = 8
+Cyclomatic complexity = 13
diff --git a/basic-cwe-examples/.frama-c/cwe190.eva/alarms.csv b/basic-cwe-examples/.frama-c/cwe190.eva/alarms.csv
index 05f9878d1a06196724c3b4c34b2531e1fb7c9599..95905c5a15f1ba20c0315210847bc0cc3fc17614 100644
--- a/basic-cwe-examples/.frama-c/cwe190.eva/alarms.csv
+++ b/basic-cwe-examples/.frama-c/cwe190.eva/alarms.csv
@@ -1,3 +1,2 @@
 directory	file	line	function	property kind	status	property
-.	cwe190.c	32	main	mem_access	Unknown	\valid(response + i)
-.	cwe190.c	39	main	mem_access	Invalid or unreachable	\valid(response + i_0)
+.	cwe190.c	44	main	mem_access	Invalid or unreachable	\valid(response + i_0)
diff --git a/basic-cwe-examples/.frama-c/cwe190.eva/metrics.log b/basic-cwe-examples/.frama-c/cwe190.eva/metrics.log
index 29e31d5217c611081a01859abf2da32fa3b8b4b2..1a73b1cf97fce111f9fef712326e73b531dfc7c9 100644
--- a/basic-cwe-examples/.frama-c/cwe190.eva/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe190.eva/metrics.log
@@ -1,12 +1,13 @@
 [metrics] Eva coverage statistics
 =======================
-Syntactically reachable functions = 4 (out of 4)
-Semantically reached functions = 4
+Syntactically reachable functions = 5 (out of 5)
+Semantically reached functions = 5
 Coverage estimation = 100.0%
 [metrics] Statements analyzed by Eva
 --------------------------
-30 stmts in analyzed functions, 25 stmts analyzed (83.3%)
-packet_get_int_ok: 2 stmts out of 2 (100.0%)
-packet_get_int_problem: 2 stmts out of 2 (100.0%)
+41 stmts in analyzed functions, 38 stmts analyzed (92.7%)
+packet_get_int_ok: 5 stmts out of 5 (100.0%)
+packet_get_int_problem: 5 stmts out of 5 (100.0%)
 packet_get_string: 2 stmts out of 2 (100.0%)
-main: 19 stmts out of 24 (79.2%)
+random_int: 1 stmts out of 1 (100.0%)
+main: 25 stmts out of 28 (89.3%)
diff --git a/basic-cwe-examples/.frama-c/cwe190.eva/nonterm.log b/basic-cwe-examples/.frama-c/cwe190.eva/nonterm.log
index 90a44fdbc0b9bcf44fc332e4283bcba2fd4444c5..02c4a2c51b6640f8a5ba8a0ed1cb4d87136160e6 100644
--- a/basic-cwe-examples/.frama-c/cwe190.eva/nonterm.log
+++ b/basic-cwe-examples/.frama-c/cwe190.eva/nonterm.log
@@ -1,2 +1,2 @@
-cwe190.c:39:[nonterm] warning: non-terminating loop
+cwe190.c:44:[nonterm] warning: non-terminating loop
 stack: main
diff --git a/basic-cwe-examples/.frama-c/cwe190.eva/warnings.log b/basic-cwe-examples/.frama-c/cwe190.eva/warnings.log
index da00dd5388186428c8382c37d78a120920bd0f33..8286bf2bea369092d4f6807e5d241c95d161ea78 100644
--- a/basic-cwe-examples/.frama-c/cwe190.eva/warnings.log
+++ b/basic-cwe-examples/.frama-c/cwe190.eva/warnings.log
@@ -1,2 +1,2 @@
-cwe190.c:39:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
+cwe190.c:44:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
diff --git a/basic-cwe-examples/.frama-c/cwe190.parse/framac.ast b/basic-cwe-examples/.frama-c/cwe190.parse/framac.ast
index c0423908914c9a7eb7ecd3ef8f06e7336fa9fbc0..9ed5602e800862fd22b0d3ffaef5595cba001491 100644
--- a/basic-cwe-examples/.frama-c/cwe190.parse/framac.ast
+++ b/basic-cwe-examples/.frama-c/cwe190.parse/framac.ast
@@ -1,17 +1,27 @@
 /* Generated by Frama-C */
 #include "stdlib.h"
+int volatile _rand;
+int random_int(void)
+{
+  return _rand;
+}
+
 int packet_get_int_ok(void)
 {
-  int __retres;
-  __retres = 123456;
-  return __retres;
+  int tmp_0;
+  int tmp;
+  tmp = random_int();
+  if (tmp) tmp_0 = 0; else tmp_0 = 123456;
+  return tmp_0;
 }
 
 int packet_get_int_problem(void)
 {
-  int __retres;
-  __retres = 1073741824;
-  return __retres;
+  int tmp_0;
+  int tmp;
+  tmp = random_int();
+  if (tmp) tmp_0 = 1073741824; else tmp_0 = 0;
+  return tmp_0;
 }
 
 char *packet_get_string(char const *s)
@@ -28,6 +38,7 @@ int main(void)
   int nresp = packet_get_int_ok();
   if (nresp > 0) {
     response = (char **)malloc((unsigned int)nresp * sizeof(char *));
+    if (! response) exit(1);
     {
       int i = 0;
       while (i < nresp) {
@@ -35,11 +46,12 @@ int main(void)
         i ++;
       }
     }
+    free((void *)response);
   }
-  free((void *)response);
   nresp = packet_get_int_problem();
   if (nresp > 0) {
     response = (char **)malloc((unsigned int)nresp * sizeof(char *));
+    if (! response) exit(1);
     {
       int i_0 = 0;
       while (i_0 < nresp) {
@@ -47,8 +59,8 @@ int main(void)
         i_0 ++;
       }
     }
+    free((void *)response);
   }
-  free((void *)response);
   __retres = 0;
   return __retres;
 }
diff --git a/basic-cwe-examples/.frama-c/cwe190.parse/metrics.log b/basic-cwe-examples/.frama-c/cwe190.parse/metrics.log
index 209600bca2c7e1edb8152cee2f378db7eb7bb346..94c58dcd1ea028aaca899819eb25a539103ff441 100644
--- a/basic-cwe-examples/.frama-c/cwe190.parse/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe190.parse/metrics.log
@@ -1,7 +1,7 @@
-[metrics] Defined functions (4)
+[metrics] Defined functions (5)
 =====================
  main (0 call); packet_get_int_ok (1 call); packet_get_int_problem (1 call);
- packet_get_string (2 calls); 
+ packet_get_string (2 calls); random_int (2 calls); 
 
 Specified-only functions (0)
 ============================
@@ -21,15 +21,15 @@ Potential entry points (1)
 
 Global metrics
 ============== 
-Sloc = 30
-Decision point = 4
-Global variables = 0
-If = 4
+Sloc = 41
+Decision point = 8
+Global variables = 1
+If = 8
 Loop = 2
 Goto = 0
-Assignment = 14
-Exit point = 4
-Function = 4
-Function call = 8
+Assignment = 18
+Exit point = 5
+Function = 5
+Function call = 12
 Pointer dereferencing = 2
-Cyclomatic complexity = 8
+Cyclomatic complexity = 13
diff --git a/basic-cwe-examples/.frama-c/cwe20-precise.eva/metrics.log b/basic-cwe-examples/.frama-c/cwe20-precise.eva/metrics.log
index e6926110496493e3dc580b22af0a711a295eed47..55cf71eb1a168c801ef89f73fd8e73b5f8abe617 100644
--- a/basic-cwe-examples/.frama-c/cwe20-precise.eva/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe20-precise.eva/metrics.log
@@ -5,5 +5,5 @@ Semantically reached functions = 1
 Coverage estimation = 100.0%
 [metrics] Statements analyzed by Eva
 --------------------------
-19 stmts in analyzed functions, 19 stmts analyzed (100.0%)
-main: 19 stmts out of 19 (100.0%)
+20 stmts in analyzed functions, 20 stmts analyzed (100.0%)
+main: 20 stmts out of 20 (100.0%)
diff --git a/basic-cwe-examples/.frama-c/cwe20-precise.parse/framac.ast b/basic-cwe-examples/.frama-c/cwe20-precise.parse/framac.ast
index 9b111bb640e6ec60d6ca8957baa4072bce502e9d..832c51ac36cde0cfbdb70caf0a5024b6423cded8 100644
--- a/basic-cwe-examples/.frama-c/cwe20-precise.parse/framac.ast
+++ b/basic-cwe-examples/.frama-c/cwe20-precise.parse/framac.ast
@@ -131,6 +131,7 @@ int main(void)
       }
     }
   board = (board_square_t *)malloc((unsigned int)(m * n) * sizeof(board_square_t));
+  free((void *)board);
   __retres = 0;
   return __retres;
 }
diff --git a/basic-cwe-examples/.frama-c/cwe20-precise.parse/metrics.log b/basic-cwe-examples/.frama-c/cwe20-precise.parse/metrics.log
index 84c0bb1bc9119389b4233f95467010549406e847..aea9a9303669d9dcee5453e7bca9e2bb4130b236 100644
--- a/basic-cwe-examples/.frama-c/cwe20-precise.parse/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe20-precise.parse/metrics.log
@@ -20,7 +20,7 @@ Potential entry points (1)
 
 Global metrics
 ============== 
-Sloc = 19
+Sloc = 20
 Decision point = 4
 Global variables = 0
 If = 4
@@ -29,6 +29,6 @@ Goto = 1
 Assignment = 4
 Exit point = 1
 Function = 1
-Function call = 11
+Function call = 12
 Pointer dereferencing = 0
 Cyclomatic complexity = 5
diff --git a/basic-cwe-examples/.frama-c/cwe20.eva/metrics.log b/basic-cwe-examples/.frama-c/cwe20.eva/metrics.log
index e6926110496493e3dc580b22af0a711a295eed47..55cf71eb1a168c801ef89f73fd8e73b5f8abe617 100644
--- a/basic-cwe-examples/.frama-c/cwe20.eva/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe20.eva/metrics.log
@@ -5,5 +5,5 @@ Semantically reached functions = 1
 Coverage estimation = 100.0%
 [metrics] Statements analyzed by Eva
 --------------------------
-19 stmts in analyzed functions, 19 stmts analyzed (100.0%)
-main: 19 stmts out of 19 (100.0%)
+20 stmts in analyzed functions, 20 stmts analyzed (100.0%)
+main: 20 stmts out of 20 (100.0%)
diff --git a/basic-cwe-examples/.frama-c/cwe20.parse/framac.ast b/basic-cwe-examples/.frama-c/cwe20.parse/framac.ast
index 9b111bb640e6ec60d6ca8957baa4072bce502e9d..832c51ac36cde0cfbdb70caf0a5024b6423cded8 100644
--- a/basic-cwe-examples/.frama-c/cwe20.parse/framac.ast
+++ b/basic-cwe-examples/.frama-c/cwe20.parse/framac.ast
@@ -131,6 +131,7 @@ int main(void)
       }
     }
   board = (board_square_t *)malloc((unsigned int)(m * n) * sizeof(board_square_t));
+  free((void *)board);
   __retres = 0;
   return __retres;
 }
diff --git a/basic-cwe-examples/.frama-c/cwe20.parse/metrics.log b/basic-cwe-examples/.frama-c/cwe20.parse/metrics.log
index 84c0bb1bc9119389b4233f95467010549406e847..aea9a9303669d9dcee5453e7bca9e2bb4130b236 100644
--- a/basic-cwe-examples/.frama-c/cwe20.parse/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe20.parse/metrics.log
@@ -20,7 +20,7 @@ Potential entry points (1)
 
 Global metrics
 ============== 
-Sloc = 19
+Sloc = 20
 Decision point = 4
 Global variables = 0
 If = 4
@@ -29,6 +29,6 @@ Goto = 1
 Assignment = 4
 Exit point = 1
 Function = 1
-Function call = 11
+Function call = 12
 Pointer dereferencing = 0
 Cyclomatic complexity = 5
diff --git a/basic-cwe-examples/.frama-c/cwe416-precise.eva/alarms.csv b/basic-cwe-examples/.frama-c/cwe416-precise.eva/alarms.csv
index e851cf8ed7d9828011c9892f15fa970d9658914c..8b44be02ae9e3469f21aa9ad9125e46fd20325b3 100644
--- a/basic-cwe-examples/.frama-c/cwe416-precise.eva/alarms.csv
+++ b/basic-cwe-examples/.frama-c/cwe416-precise.eva/alarms.csv
@@ -1,7 +1,3 @@
 directory	file	line	function	property kind	status	property
-.	cwe416.c	23	main	dangling_pointer	Unknown	¬\dangling(&buf2R1)
-.	cwe416.c	23	main	mem_access	Unknown	\valid_read(argv + 1)
-.	cwe416.c	23	main	precondition of strncpy	Invalid or unreachable	room_nstring: \valid(dest + (0 .. n - 1))
-.	cwe416.c	23	main	precondition of strncpy	Unknown	valid_nstring_src: valid_read_nstring(src, n)
-FRAMAC_SHARE/libc	string.h	363	strncpy	precondition	Unknown	valid_nstring_src: valid_read_nstring(src, n)
-FRAMAC_SHARE/libc	string.h	364	strncpy	precondition	Invalid or unreachable	room_nstring: \valid(dest + (0 .. n - 1))
+.	cwe416.c	27	main	dangling_pointer	Invalid or unreachable	¬\dangling(&buf2R1)
+.	cwe416.c	27	main	mem_access	Unknown	\valid_read(argv + 1)
diff --git a/basic-cwe-examples/.frama-c/cwe416-precise.eva/metrics.log b/basic-cwe-examples/.frama-c/cwe416-precise.eva/metrics.log
index 0e6e5e33ce377a712492057b00ae2df9db7f0bf9..e1d3abc93b8c286b8542941226f3781db30287fd 100644
--- a/basic-cwe-examples/.frama-c/cwe416-precise.eva/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe416-precise.eva/metrics.log
@@ -5,5 +5,5 @@ Semantically reached functions = 1
 Coverage estimation = 100.0%
 [metrics] Statements analyzed by Eva
 --------------------------
-11 stmts in analyzed functions, 6 stmts analyzed (54.5%)
-main: 6 stmts out of 11 (54.5%)
+19 stmts in analyzed functions, 14 stmts analyzed (73.7%)
+main: 14 stmts out of 19 (73.7%)
diff --git a/basic-cwe-examples/.frama-c/cwe416-precise.eva/nonterm.log b/basic-cwe-examples/.frama-c/cwe416-precise.eva/nonterm.log
index d090b734e364b27c7477239d259b5d23aa0125c1..8f94f04c820c7d66da7bc8731c6781d8801c96a5 100644
--- a/basic-cwe-examples/.frama-c/cwe416-precise.eva/nonterm.log
+++ b/basic-cwe-examples/.frama-c/cwe416-precise.eva/nonterm.log
@@ -1,2 +1,2 @@
-cwe416.c:23:[nonterm] warning: non-terminating function call
+cwe416.c:27:[nonterm] warning: non-terminating function call
 stack: main
diff --git a/basic-cwe-examples/.frama-c/cwe416-precise.parse/framac.ast b/basic-cwe-examples/.frama-c/cwe416-precise.parse/framac.ast
index 9dd04d5530e7b65f5404d1f889db51afd5a47c75..f036f7c092d9d724f1d8b42fc7e6ad565974775a 100644
--- a/basic-cwe-examples/.frama-c/cwe416-precise.parse/framac.ast
+++ b/basic-cwe-examples/.frama-c/cwe416-precise.parse/framac.ast
@@ -15,10 +15,14 @@ int main(int argc, char **argv)
   char *buf2R2;
   char *buf3R2;
   buf1R1 = (char *)malloc((unsigned int)512);
+  if (! buf1R1) exit(1);
   buf2R1 = (char *)malloc((unsigned int)512);
+  if (! buf2R1) exit(1);
   free((void *)buf2R1);
   buf2R2 = (char *)malloc((unsigned int)(512 / 2 - 8));
+  if (! buf2R2) exit(1);
   buf3R2 = (char *)malloc((unsigned int)(512 / 2 - 8));
+  if (! buf3R2) exit(1);
   strncpy(buf2R1,(char const *)*(argv + 1),(unsigned int)(512 - 1));
   free((void *)buf1R1);
   free((void *)buf2R2);
diff --git a/basic-cwe-examples/.frama-c/cwe416-precise.parse/metrics.log b/basic-cwe-examples/.frama-c/cwe416-precise.parse/metrics.log
index d284d821861deb137ffc55b98271d9acf2eb7446..b69d6dc03c40eb1b60bd386c49c759c4f2596fea 100644
--- a/basic-cwe-examples/.frama-c/cwe416-precise.parse/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe416-precise.parse/metrics.log
@@ -20,15 +20,15 @@ Potential entry points (1)
 
 Global metrics
 ============== 
-Sloc = 11
-Decision point = 0
+Sloc = 19
+Decision point = 4
 Global variables = 0
-If = 0
+If = 4
 Loop = 0
 Goto = 0
 Assignment = 5
 Exit point = 1
 Function = 1
-Function call = 9
+Function call = 13
 Pointer dereferencing = 1
-Cyclomatic complexity = 1
+Cyclomatic complexity = 5
diff --git a/basic-cwe-examples/.frama-c/cwe416.eva/alarms.csv b/basic-cwe-examples/.frama-c/cwe416.eva/alarms.csv
index 1a2df76a541a74842a229045b7b3eccf79d42a46..8b44be02ae9e3469f21aa9ad9125e46fd20325b3 100644
--- a/basic-cwe-examples/.frama-c/cwe416.eva/alarms.csv
+++ b/basic-cwe-examples/.frama-c/cwe416.eva/alarms.csv
@@ -1,7 +1,3 @@
 directory	file	line	function	property kind	status	property
-.	cwe416.c	23	main	dangling_pointer	Unknown	¬\dangling(&buf2R1)
-.	cwe416.c	23	main	mem_access	Unknown	\valid_read(argv + 1)
-.	cwe416.c	23	main	precondition of strncpy	Unknown	room_nstring: \valid(dest + (0 .. n - 1))
-.	cwe416.c	23	main	precondition of strncpy	Unknown	valid_nstring_src: valid_read_nstring(src, n)
-FRAMAC_SHARE/libc	string.h	363	strncpy	precondition	Unknown	valid_nstring_src: valid_read_nstring(src, n)
-FRAMAC_SHARE/libc	string.h	364	strncpy	precondition	Unknown	room_nstring: \valid(dest + (0 .. n - 1))
+.	cwe416.c	27	main	dangling_pointer	Invalid or unreachable	¬\dangling(&buf2R1)
+.	cwe416.c	27	main	mem_access	Unknown	\valid_read(argv + 1)
diff --git a/basic-cwe-examples/.frama-c/cwe416.eva/metrics.log b/basic-cwe-examples/.frama-c/cwe416.eva/metrics.log
index cb1beb046afcd763f2a25312594c7ebe1e25fe9f..e1d3abc93b8c286b8542941226f3781db30287fd 100644
--- a/basic-cwe-examples/.frama-c/cwe416.eva/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe416.eva/metrics.log
@@ -5,5 +5,5 @@ Semantically reached functions = 1
 Coverage estimation = 100.0%
 [metrics] Statements analyzed by Eva
 --------------------------
-11 stmts in analyzed functions, 11 stmts analyzed (100.0%)
-main: 11 stmts out of 11 (100.0%)
+19 stmts in analyzed functions, 14 stmts analyzed (73.7%)
+main: 14 stmts out of 19 (73.7%)
diff --git a/basic-cwe-examples/.frama-c/cwe416.eva/nonterm.log b/basic-cwe-examples/.frama-c/cwe416.eva/nonterm.log
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..8f94f04c820c7d66da7bc8731c6781d8801c96a5 100644
--- a/basic-cwe-examples/.frama-c/cwe416.eva/nonterm.log
+++ b/basic-cwe-examples/.frama-c/cwe416.eva/nonterm.log
@@ -0,0 +1,2 @@
+cwe416.c:27:[nonterm] warning: non-terminating function call
+stack: main
diff --git a/basic-cwe-examples/.frama-c/cwe416.parse/framac.ast b/basic-cwe-examples/.frama-c/cwe416.parse/framac.ast
index 9dd04d5530e7b65f5404d1f889db51afd5a47c75..f036f7c092d9d724f1d8b42fc7e6ad565974775a 100644
--- a/basic-cwe-examples/.frama-c/cwe416.parse/framac.ast
+++ b/basic-cwe-examples/.frama-c/cwe416.parse/framac.ast
@@ -15,10 +15,14 @@ int main(int argc, char **argv)
   char *buf2R2;
   char *buf3R2;
   buf1R1 = (char *)malloc((unsigned int)512);
+  if (! buf1R1) exit(1);
   buf2R1 = (char *)malloc((unsigned int)512);
+  if (! buf2R1) exit(1);
   free((void *)buf2R1);
   buf2R2 = (char *)malloc((unsigned int)(512 / 2 - 8));
+  if (! buf2R2) exit(1);
   buf3R2 = (char *)malloc((unsigned int)(512 / 2 - 8));
+  if (! buf3R2) exit(1);
   strncpy(buf2R1,(char const *)*(argv + 1),(unsigned int)(512 - 1));
   free((void *)buf1R1);
   free((void *)buf2R2);
diff --git a/basic-cwe-examples/.frama-c/cwe416.parse/metrics.log b/basic-cwe-examples/.frama-c/cwe416.parse/metrics.log
index d284d821861deb137ffc55b98271d9acf2eb7446..b69d6dc03c40eb1b60bd386c49c759c4f2596fea 100644
--- a/basic-cwe-examples/.frama-c/cwe416.parse/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe416.parse/metrics.log
@@ -20,15 +20,15 @@ Potential entry points (1)
 
 Global metrics
 ============== 
-Sloc = 11
-Decision point = 0
+Sloc = 19
+Decision point = 4
 Global variables = 0
-If = 0
+If = 4
 Loop = 0
 Goto = 0
 Assignment = 5
 Exit point = 1
 Function = 1
-Function call = 9
+Function call = 13
 Pointer dereferencing = 1
-Cyclomatic complexity = 1
+Cyclomatic complexity = 5
diff --git a/basic-cwe-examples/.frama-c/cwe787-precise.eva/alarms.csv b/basic-cwe-examples/.frama-c/cwe787-precise.eva/alarms.csv
index 9d7be6d0b5def26c94b063a9979691e3330b3644..452f2812f4a45788c40f44c6384911161878d8f7 100644
--- a/basic-cwe-examples/.frama-c/cwe787-precise.eva/alarms.csv
+++ b/basic-cwe-examples/.frama-c/cwe787-precise.eva/alarms.csv
@@ -1,2 +1,2 @@
 directory	file	line	function	property kind	status	property
-.	cwe787.c	29	copy_input	mem_access	Unknown	\valid(dst_buf + tmp_5)
+.	cwe787.c	26	copy_input	mem_access	Unknown	\valid(dst_buf + tmp_5)
diff --git a/basic-cwe-examples/.frama-c/cwe787-precise.eva/metrics.log b/basic-cwe-examples/.frama-c/cwe787-precise.eva/metrics.log
index f6a2b08b83511c7bf93164322daf629706e4ccec..80b221b258dab55dd845eaf94106006dc66e04ba 100644
--- a/basic-cwe-examples/.frama-c/cwe787-precise.eva/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe787-precise.eva/metrics.log
@@ -5,6 +5,6 @@ Semantically reached functions = 2
 Coverage estimation = 100.0%
 [metrics] Statements analyzed by Eva
 --------------------------
-59 stmts in analyzed functions, 56 stmts analyzed (94.9%)
-copy_input: 52 stmts out of 53 (98.1%)
-main: 4 stmts out of 6 (66.7%)
+63 stmts in analyzed functions, 59 stmts analyzed (93.7%)
+copy_input: 54 stmts out of 55 (98.2%)
+main: 5 stmts out of 8 (62.5%)
diff --git a/basic-cwe-examples/.frama-c/cwe787-precise.eva/nonterm.log b/basic-cwe-examples/.frama-c/cwe787-precise.eva/nonterm.log
index 93f8bef44496e9d6118b2dc73f1b1c346d4931a8..b16304bfa1b733c53696493b0546e6fdf65e03dd 100644
--- a/basic-cwe-examples/.frama-c/cwe787-precise.eva/nonterm.log
+++ b/basic-cwe-examples/.frama-c/cwe787-precise.eva/nonterm.log
@@ -1,3 +1,3 @@
-cwe787.c:23:[nonterm] warning: non-terminating loop
-stack: copy_input :: cwe787.c:45 <- main
-cwe787.c:46:[nonterm] warning: unreachable return
+cwe787.c:20:[nonterm] warning: non-terminating loop
+stack: copy_input :: cwe787.c:42 <- main
+cwe787.c:43:[nonterm] warning: unreachable return
diff --git a/basic-cwe-examples/.frama-c/cwe787-precise.eva/warnings.log b/basic-cwe-examples/.frama-c/cwe787-precise.eva/warnings.log
index 8abb70980fe47691ccdd7fb13c1134921cb33d3e..bd08b209dcd4c239255edda9f5f78358b55dfe28 100644
--- a/basic-cwe-examples/.frama-c/cwe787-precise.eva/warnings.log
+++ b/basic-cwe-examples/.frama-c/cwe787-precise.eva/warnings.log
@@ -1,2 +1,2 @@
-cwe787.c:29:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
-stack: copy_input :: cwe787.c:45 <- main
+cwe787.c:26:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
+stack: copy_input :: cwe787.c:42 <- main
diff --git a/basic-cwe-examples/.frama-c/cwe787-precise.parse/framac.ast b/basic-cwe-examples/.frama-c/cwe787-precise.parse/framac.ast
index f583df23361c6c29cb3c54c930796414bca5cdef..3a9b0588f6a40b7758645979b0215c7922323d23 100644
--- a/basic-cwe-examples/.frama-c/cwe787-precise.parse/framac.ast
+++ b/basic-cwe-examples/.frama-c/cwe787-precise.parse/framac.ast
@@ -9,6 +9,7 @@ char *copy_input(char *user_supplied_string)
   size_t tmp_0;
   char *dst_buf =
     malloc(((unsigned int)4 * sizeof(char)) * (unsigned int)16);
+  if (! dst_buf) exit(1);
   tmp_0 = strlen((char const *)user_supplied_string);
   if ((size_t)16 <= tmp_0) exit(1);
   dst_index = 0;
@@ -69,10 +70,14 @@ char *copy_input(char *user_supplied_string)
 int main(void)
 {
   int __retres;
+  char *tmp;
+  char *tmp_0;
   char *benevolent_string = (char *)"<a href=\'ab&c\'>";
-  copy_input(benevolent_string);
+  tmp = copy_input(benevolent_string);
+  free((void *)tmp);
   char *malicious_string = (char *)"&&&&&&&&&&&&&&&";
-  copy_input(malicious_string);
+  tmp_0 = copy_input(malicious_string);
+  free((void *)tmp_0);
   __retres = 0;
   return __retres;
 }
diff --git a/basic-cwe-examples/.frama-c/cwe787-precise.parse/metrics.log b/basic-cwe-examples/.frama-c/cwe787-precise.parse/metrics.log
index 5993c9e945633bafe1f5facd1d0c29ef7a332c31..c31eb0daef87aa3f83e68217d8a9432442ef956d 100644
--- a/basic-cwe-examples/.frama-c/cwe787-precise.parse/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe787-precise.parse/metrics.log
@@ -20,15 +20,15 @@ Potential entry points (1)
 
 Global metrics
 ============== 
-Sloc = 59
-Decision point = 4
+Sloc = 63
+Decision point = 5
 Global variables = 0
-If = 4
+If = 5
 Loop = 1
 Goto = 0
-Assignment = 36
+Assignment = 38
 Exit point = 2
 Function = 2
-Function call = 6
+Function call = 9
 Pointer dereferencing = 12
-Cyclomatic complexity = 6
+Cyclomatic complexity = 7
diff --git a/basic-cwe-examples/.frama-c/cwe787.eva/alarms.csv b/basic-cwe-examples/.frama-c/cwe787.eva/alarms.csv
index 0d5866ed7a65c930a56ecbe3237be382f56cfab5..7c25eae88e2f12612033000abf8eb8f636c0edd8 100644
--- a/basic-cwe-examples/.frama-c/cwe787.eva/alarms.csv
+++ b/basic-cwe-examples/.frama-c/cwe787.eva/alarms.csv
@@ -1,19 +1,19 @@
 directory	file	line	function	property kind	status	property
+.	cwe787.c	22	copy_input	signed_overflow	Unknown	dst_index + 1 ≤ 2147483647
+.	cwe787.c	22	copy_input	mem_access	Unknown	\valid(dst_buf + tmp_1)
+.	cwe787.c	23	copy_input	signed_overflow	Unknown	dst_index + 1 ≤ 2147483647
+.	cwe787.c	23	copy_input	mem_access	Unknown	\valid(dst_buf + tmp_2)
+.	cwe787.c	24	copy_input	signed_overflow	Unknown	dst_index + 1 ≤ 2147483647
+.	cwe787.c	24	copy_input	mem_access	Unknown	\valid(dst_buf + tmp_3)
 .	cwe787.c	25	copy_input	signed_overflow	Unknown	dst_index + 1 ≤ 2147483647
-.	cwe787.c	25	copy_input	mem_access	Unknown	\valid(dst_buf + tmp_1)
+.	cwe787.c	25	copy_input	mem_access	Unknown	\valid(dst_buf + tmp_4)
 .	cwe787.c	26	copy_input	signed_overflow	Unknown	dst_index + 1 ≤ 2147483647
-.	cwe787.c	26	copy_input	mem_access	Unknown	\valid(dst_buf + tmp_2)
-.	cwe787.c	27	copy_input	signed_overflow	Unknown	dst_index + 1 ≤ 2147483647
-.	cwe787.c	27	copy_input	mem_access	Unknown	\valid(dst_buf + tmp_3)
-.	cwe787.c	28	copy_input	signed_overflow	Unknown	dst_index + 1 ≤ 2147483647
-.	cwe787.c	28	copy_input	mem_access	Unknown	\valid(dst_buf + tmp_4)
+.	cwe787.c	26	copy_input	mem_access	Unknown	\valid(dst_buf + tmp_5)
 .	cwe787.c	29	copy_input	signed_overflow	Unknown	dst_index + 1 ≤ 2147483647
-.	cwe787.c	29	copy_input	mem_access	Unknown	\valid(dst_buf + tmp_5)
-.	cwe787.c	32	copy_input	signed_overflow	Unknown	dst_index + 1 ≤ 2147483647
-.	cwe787.c	32	copy_input	mem_access	Unknown	\valid(dst_buf + tmp_6)
+.	cwe787.c	29	copy_input	mem_access	Unknown	\valid(dst_buf + tmp_6)
+.	cwe787.c	30	copy_input	signed_overflow	Unknown	dst_index + 1 ≤ 2147483647
+.	cwe787.c	30	copy_input	mem_access	Unknown	\valid(dst_buf + tmp_7)
+.	cwe787.c	31	copy_input	signed_overflow	Unknown	dst_index + 1 ≤ 2147483647
+.	cwe787.c	31	copy_input	mem_access	Unknown	\valid(dst_buf + tmp_8)
 .	cwe787.c	33	copy_input	signed_overflow	Unknown	dst_index + 1 ≤ 2147483647
-.	cwe787.c	33	copy_input	mem_access	Unknown	\valid(dst_buf + tmp_7)
-.	cwe787.c	34	copy_input	signed_overflow	Unknown	dst_index + 1 ≤ 2147483647
-.	cwe787.c	34	copy_input	mem_access	Unknown	\valid(dst_buf + tmp_8)
-.	cwe787.c	36	copy_input	signed_overflow	Unknown	dst_index + 1 ≤ 2147483647
-.	cwe787.c	36	copy_input	mem_access	Unknown	\valid(dst_buf + tmp_9)
+.	cwe787.c	33	copy_input	mem_access	Unknown	\valid(dst_buf + tmp_9)
diff --git a/basic-cwe-examples/.frama-c/cwe787.eva/metrics.log b/basic-cwe-examples/.frama-c/cwe787.eva/metrics.log
index 0c237d4f07e403178abf7a7358728060aec197f9..b21ec892c4c6994e34e86fe289726c600de553b1 100644
--- a/basic-cwe-examples/.frama-c/cwe787.eva/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe787.eva/metrics.log
@@ -5,6 +5,6 @@ Semantically reached functions = 2
 Coverage estimation = 100.0%
 [metrics] Statements analyzed by Eva
 --------------------------
-59 stmts in analyzed functions, 58 stmts analyzed (98.3%)
-main: 6 stmts out of 6 (100.0%)
-copy_input: 52 stmts out of 53 (98.1%)
+63 stmts in analyzed functions, 62 stmts analyzed (98.4%)
+main: 8 stmts out of 8 (100.0%)
+copy_input: 54 stmts out of 55 (98.2%)
diff --git a/basic-cwe-examples/.frama-c/cwe787.parse/framac.ast b/basic-cwe-examples/.frama-c/cwe787.parse/framac.ast
index f583df23361c6c29cb3c54c930796414bca5cdef..3a9b0588f6a40b7758645979b0215c7922323d23 100644
--- a/basic-cwe-examples/.frama-c/cwe787.parse/framac.ast
+++ b/basic-cwe-examples/.frama-c/cwe787.parse/framac.ast
@@ -9,6 +9,7 @@ char *copy_input(char *user_supplied_string)
   size_t tmp_0;
   char *dst_buf =
     malloc(((unsigned int)4 * sizeof(char)) * (unsigned int)16);
+  if (! dst_buf) exit(1);
   tmp_0 = strlen((char const *)user_supplied_string);
   if ((size_t)16 <= tmp_0) exit(1);
   dst_index = 0;
@@ -69,10 +70,14 @@ char *copy_input(char *user_supplied_string)
 int main(void)
 {
   int __retres;
+  char *tmp;
+  char *tmp_0;
   char *benevolent_string = (char *)"<a href=\'ab&c\'>";
-  copy_input(benevolent_string);
+  tmp = copy_input(benevolent_string);
+  free((void *)tmp);
   char *malicious_string = (char *)"&&&&&&&&&&&&&&&";
-  copy_input(malicious_string);
+  tmp_0 = copy_input(malicious_string);
+  free((void *)tmp_0);
   __retres = 0;
   return __retres;
 }
diff --git a/basic-cwe-examples/.frama-c/cwe787.parse/metrics.log b/basic-cwe-examples/.frama-c/cwe787.parse/metrics.log
index 5993c9e945633bafe1f5facd1d0c29ef7a332c31..c31eb0daef87aa3f83e68217d8a9432442ef956d 100644
--- a/basic-cwe-examples/.frama-c/cwe787.parse/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe787.parse/metrics.log
@@ -20,15 +20,15 @@ Potential entry points (1)
 
 Global metrics
 ============== 
-Sloc = 59
-Decision point = 4
+Sloc = 63
+Decision point = 5
 Global variables = 0
-If = 4
+If = 5
 Loop = 1
 Goto = 0
-Assignment = 36
+Assignment = 38
 Exit point = 2
 Function = 2
-Function call = 6
+Function call = 9
 Pointer dereferencing = 12
-Cyclomatic complexity = 6
+Cyclomatic complexity = 7
diff --git a/basic-cwe-examples/Makefile b/basic-cwe-examples/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..824e4eb4e3be3232ce5d3ae0c5b209da6a57df78
--- /dev/null
+++ b/basic-cwe-examples/Makefile
@@ -0,0 +1,11 @@
+TARGETS=cwe20 cwe119 cwe190 cwe416 cwe787
+
+all: $(TARGETS)
+
+clean:
+	rm -f $(TARGETS)
+
+CFLAGS ?= -Wall
+
+%: %.c
+	$(CC) $(CFLAGS) -o $@ $^
diff --git a/basic-cwe-examples/cwe119.c b/basic-cwe-examples/cwe119.c
index cfbaa1a82789d451d327ee9980918a219a771ff7..dcb45176019b7ee2e1460cbc3899055700fca59c 100644
--- a/basic-cwe-examples/cwe119.c
+++ b/basic-cwe-examples/cwe119.c
@@ -1,15 +1,18 @@
 // Based on MITRE's CWE-119, demonstrative example 1
 // https://cwe.mitre.org/data/definitions/119.html
 
-// Run with "-eva-precision 1" to obtain a "Red Alarm".
-
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
 #include <netdb.h>
 
-// To use Frama-C's "Frama_C_interval" to generate a nondeterministic value
-#include "__fc_builtin.h"
+volatile uint32_t _rand;
+// returns a random non-zero uint32_t
+uint32_t nonzero_uint32_t(void) {
+  uint32_t r = _rand;
+  if (!r) return 1U;
+  else return r;
+}
 
 static void validate_addr_form(char *v) {
   // naive, simplistic validation
@@ -33,7 +36,7 @@ static in_addr_t my_inet_addr(const char *cp) {
   if (my_strcmp(cp, "127.0.0.1") == 0) {
     return 0;
   } else {
-    return Frama_C_nondet(1,UINT_MAX);
+    return nonzero_uint32_t();
   }
 }
 
@@ -52,13 +55,13 @@ static struct hostent *my_gethostbyaddr(const void *addr,
 
 void host_lookup(char *user_supplied_addr){
   struct hostent *hp;
-  in_addr_t *addr;
+  in_addr_t addr;
   char hostname[64];
 
   /* routine that ensures user_supplied_addr is in the right format for conversion */
   validate_addr_form(user_supplied_addr);
   addr = my_inet_addr(user_supplied_addr);
-  hp = my_gethostbyaddr(addr, sizeof(struct in_addr), AF_INET);
+  hp = my_gethostbyaddr(&addr, sizeof(struct in_addr), AF_INET);
   strcpy(hostname, hp->h_name);
 }
 
diff --git a/basic-cwe-examples/cwe190.c b/basic-cwe-examples/cwe190.c
index ff56da6bd5ed0920603ade2c86b985dbff74c1fb..e303db70153ac167c0dede63a448d5130f3de56c 100644
--- a/basic-cwe-examples/cwe190.c
+++ b/basic-cwe-examples/cwe190.c
@@ -6,18 +6,21 @@
 // write to the (under-allocated) buffer.
 // Adding option "-warn-unsigned-overflow" ensures Eva reports the
 // overflow as soon as it happens.
-// Also, adding option "-eva-no-alloc-returns-null" allows focusing on this
-// issue while ignoring the the fact that malloc() may fail (which would
-// require an extra check).
 
 #include <stdlib.h>
 
+volatile int _rand;
+// returns a random int
+int random_int(void) {
+  return _rand;
+}
+
 int packet_get_int_ok() {
-  return 123456;
+  return random_int() ? 0 : 123456; // ok size
 }
 
 int packet_get_int_problem() {
-  return 1073741824;
+  return random_int() ? 1073741824 : 0; // too large (>= INT_MAX/4)
 }
 
 char *packet_get_string(const char *s) {
@@ -29,15 +32,17 @@ int main() {
   int nresp = packet_get_int_ok();
   if (nresp > 0) {
     response = malloc(nresp*sizeof(char*));
+    if (!response) exit(1);
     for (int i = 0; i < nresp; i++) response[i] = packet_get_string(NULL);
+    free(response);
   }
-  free(response);
 
   nresp = packet_get_int_problem();
   if (nresp > 0) {
     response = malloc(nresp*sizeof(char*));
+    if (!response) exit(1);
     for (int i = 0; i < nresp; i++) response[i] = packet_get_string(NULL);
+    free(response);
   }
-  free(response);
   return 0;
 }
diff --git a/basic-cwe-examples/cwe20.c b/basic-cwe-examples/cwe20.c
index 4a991fd2bf21cb53e52325fc6a202eaae59412ca..e10512d78f4e8945cf80aeb662c0700f0b788267 100644
--- a/basic-cwe-examples/cwe20.c
+++ b/basic-cwe-examples/cwe20.c
@@ -33,5 +33,6 @@ int main() {
   }
   board = (board_square_t*) malloc( m * n * sizeof(board_square_t));
 
+  free(board);
   return 0;
 }
diff --git a/basic-cwe-examples/cwe416.c b/basic-cwe-examples/cwe416.c
index 69ab349a35b0e69d5666348b336a08bb85b4c787..255731555dbfe90715327d23c8704a303a9d1b31 100644
--- a/basic-cwe-examples/cwe416.c
+++ b/basic-cwe-examples/cwe416.c
@@ -16,10 +16,14 @@ int main(int argc, char **argv) {
   char *buf2R2;
   char *buf3R2;
   buf1R1 = (char *) malloc(BUFSIZER1);
+  if (!buf1R1) exit(1);
   buf2R1 = (char *) malloc(BUFSIZER1);
+  if (!buf2R1) exit(1);
   free(buf2R1);
   buf2R2 = (char *) malloc(BUFSIZER2);
+  if (!buf2R2) exit(1);
   buf3R2 = (char *) malloc(BUFSIZER2);
+  if (!buf3R2) exit(1);
   strncpy(buf2R1, argv[1], BUFSIZER1-1);
   free(buf1R1);
   free(buf2R2);
diff --git a/basic-cwe-examples/cwe787.c b/basic-cwe-examples/cwe787.c
index 7086b0b3727ec7f294584b889b7f1741c31ce5c5..e31f5a0e268f2d30c3ab0ccbbe02421e6c5dec82 100644
--- a/basic-cwe-examples/cwe787.c
+++ b/basic-cwe-examples/cwe787.c
@@ -4,10 +4,6 @@
 // Option "-eva-precision 1" reduces the number of "Unknown" alarms.
 // Run with "-eva-precision 2" to obtain a "Red Alarm".
 
-// Also, adding option "-eva-no-alloc-returns-null" allows focusing on this
-// issue while ignoring the the fact that malloc() may fail (which would
-// require an extra check).
-
 #include <stdlib.h>
 #include <string.h>
 
@@ -16,6 +12,7 @@
 char * copy_input(char *user_supplied_string) {
   int i, dst_index;
   char *dst_buf = (char*)malloc(4*sizeof(char) * MAX_SIZE);
+  if (!dst_buf) exit(1);
   if ( MAX_SIZE <= strlen(user_supplied_string) ){
     exit(1);
   }
@@ -40,8 +37,8 @@ char * copy_input(char *user_supplied_string) {
 
 int main() {
   char *benevolent_string = "<a href='ab&c'>";
-  copy_input(benevolent_string);
+  free(copy_input(benevolent_string));
   char *malicious_string  = "&&&&&&&&&&&&&&&";
-  copy_input(malicious_string);
+  free(copy_input(malicious_string));
   return 0;
 }