diff --git a/ALL_VERSIONS b/ALL_VERSIONS
index fc52ef5a8b9d32b8cf11068cdc80efb2e90f3334..a9ea55e97ca8ea0caa32a629a68eb01eaab48e61 100644
--- a/ALL_VERSIONS
+++ b/ALL_VERSIONS
@@ -1,5 +1,7 @@
Version number Date of release Notes
============== =============== =====
+Silicon-20161101 2016, December 2
+
Aluminium-20160502 2016, May 31
Aluminium-20160501 2016, May 30 Removed
Aluminium-rc1 2016, May 13 Not publicly released
diff --git a/Changelog b/Changelog
index d3cf78b53d5d24dd74cf0c2c8ff679cf96014340..9b7a9a242fedc82bf6eeb11cdf205bcc327cee3a 100644
--- a/Changelog
+++ b/Changelog
@@ -14,7 +14,7 @@
###############################################################################
######################################
-Open Source Release <next-next-release>
+Open Source Release <next-release>
######################################
- Rte [2016/11/25] Remove option -rte-all.
@@ -34,35 +34,37 @@ Open Source Release <next-next-release>
specifiers (support for CERT DCL-36-C coding rule)
######################################
-Open Source Release <next-release>
+Open Source Release Silicon-20161101
######################################
-*! Eva [2016/10/29] Fix soundness bug on statements with RTE or
programmatically-added user assertions (bts #2258). This
leads to minor changes in the way states are propagated when
- all slevel has been consumed.
+ all slevel has been consumed. Also, consolidated states now
+ return the abstraction before any reduction by assertions or
+ alarms.
-* Eva [2016/10/20] Fix bug in the bitwise domain, on some applications
of the & and | operators
- Value [2016/10/20] New (experimental) option -val-builtins-auto, to
automatically replace known C functions by builtins. Will
be set by default in Phosphorus.
-* Value [2016/10/19] Frama_C_cos and Frama_C_sin builtins are now
- precise by default. The former Frama_C_cos/sin_precise have been
- removed
+ precise by default. The former Frama_C_cos / Frama_Csin_precise
+ have been removed
-* Kernel [2016/10/18] Fix bug when pretty printing an ACSL term
"divisor / *p" (bts #2250).
- Eva [2016/10/18] New experimental Gauges domain, that relates
integer variable to loop counters.
-! Kernel [2016/10/15] Fix major bug in the backward dataflow of module
Dataflows
--! Scope [2016/10/15] Fix bug that might lead to unsoundness and/or looping
- in 'Datascope' functionality (#!235)
+-! Scope [2016/10/15] Fix bug that might lead to unsoundness and / or
+ looping in 'Datascope' functionality (#!235)
-* Eva [2016/10/11] Prevent incorrect reductions on memory locations
with volatile qualifier
-! Value [2016/10/11] Option -val-warn-copy-indeterminate is now set by
default. See command-line help if you want to deactivate it.
- Kernel [2016/10/07] Fix bug that may occur when modifying several times
- command line-options taking functions in argument (issue #@109)
+ command line-options taking functions as argument (issue #@109)
-! Libc [2016/10/07] Functions in share/libc.c have been inlined into
the proper .c files under share/libc
- Eva [2016/10/07] More systematic backward-propagation between
@@ -82,7 +84,7 @@ Open Source Release <next-release>
are now evaluated by Value
-* Eva [2016/09/18] Fix bug in equality domain, after assignements
lv = e where the modified locations intersect those involved in
- computing l
+ computing lv
-* Eva [2016/09/18] fix performance bug in the equality domain,
especially visible on programs with many local variables.
o! Kernel [2016/09/16] Rename some types of the logic AST for more coherence
@@ -94,7 +96,6 @@ o! Kernel [2016/09/16] Rename some types of the logic AST for more coherence
-! Libc [2016/08/29] New file share/libc/string.c, with simple
implementations for C99 functions defined in string.h.
Duplicate implementations were removed from share/libc.c.
-- Kernel [2016/08/26] Support for C11 typedef redefinitions
-* Kernel [2016/08/12] Fix bug #2239 about unsoundness of callgraph's
services computation (bug introduced in Frama-C Magnesium).
o! Kernel [2016/07/26] Suppress return_stmt field of kernel_function type.
@@ -137,8 +138,8 @@ o! Kernel [2016/06/14] Remove class Filecheck.check from API.
prefixed by [value] instead of [kernel]
- Value [2016/05/31] New message key 'garbled-mix', to track garbled mix
generated during the analysis
--* Value [2016/05/30] Garbled mix created when analysis assigns/clause
- are now tagged as having "Library function" origin
+-* Value [2016/05/30] Garbled mix created when analyzing assigns / from
+ clauses are now tagged as having "Library function" origin
- Value [2016/05/30] New option -val-warn-on-alarms, which governs
whether alarms are printed as warnings or text.
-* Kernel [2016/05/23] Side-effect free instructions such as 'e;' are now
diff --git a/VERSION b/VERSION
index a25fe83fbb9fe2a97a0f133ee226401c15e57b27..515faf39c17ac0dac1b7d51251ef7da3ad6685f2 100644
--- a/VERSION
+++ b/VERSION
@@ -1 +1 @@
-Silicium-rc1
\ No newline at end of file
+Silicon-20161101+dev
\ No newline at end of file
diff --git a/bin/build-src-distrib.sh b/bin/build-src-distrib.sh
index 59069a51415e4387b191f55de0029926f34e0c26..8604531268804651ed130a4d264e0195f122d460 100755
--- a/bin/build-src-distrib.sh
+++ b/bin/build-src-distrib.sh
@@ -97,7 +97,7 @@ case "${STEP}" in
run "git worktree add --detach $BUILD_DIR $FRAMAC_BRANCH"
run "cd $BUILD_DIR; autoconf"
run "cd $BUILD_DIR; ./configure"
- run "cd $BUILD_DIR; make OPEN_SOURCE=yes src-distrib"
+ run "cd $BUILD_DIR; make -j OPEN_SOURCE=yes src-distrib"
SPEC_FILE="$DOWNLOAD_DIR/frama-c-${FRAMAC_VERSION}.tar.gz"
run "rm -f $WEBSITE_DIR/$SPEC_FILE"
run "cp $BUILD_DIR/frama-c-${FRAMAC_VERSION}.tar.gz $WEBSITE_DIR/$SPEC_FILE"
@@ -107,7 +107,7 @@ case "${STEP}" in
;&
4)
step 4 "BUILDING THE API BUNDLE"
- run "cd $BUILD_DIR; make doc-distrib"
+ run "cd $BUILD_DIR; make -j doc-distrib"
SPEC_FILE="$DOWNLOAD_DIR/frama-c-${FRAMAC_VERSION}_api.tar.gz"
run "rm -f $WEBSITE_DIR/$SPEC_FILE"
run "cp $BUILD_DIR/frama-c-api.tar.gz $WEBSITE_DIR/$SPEC_FILE"
diff --git a/doc/build-manuals.sh b/doc/build-manuals.sh
index 758e3a7db55ee734b23ed315e3af9106e18eb29c..48bae4580078ed0ce401e3f8170ccfc0cc36264e 100755
--- a/doc/build-manuals.sh
+++ b/doc/build-manuals.sh
@@ -18,12 +18,12 @@ mkdir -p manuals
build userman
build developer
-build speclang
build rte
build aorai
build metrics
build value
+build acsl
cd ../src/plugins/wp/doc/
diff --git a/doc/changelog/Makefile b/doc/changelog/Makefile
deleted file mode 100644
index f0d9b5faa12eb345d1ce77e37fca4709c7928890..0000000000000000000000000000000000000000
--- a/doc/changelog/Makefile
+++ /dev/null
@@ -1,41 +0,0 @@
-##########################################################################
-# #
-# This file is part of Frama-C. #
-# #
-# Copyright (C) 2007-2016 #
-# CEA (Commissariat à l'énergie atomique et aux énergies #
-# alternatives) #
-# #
-# All rights reserved. #
-# Contact CEA LIST for licensing. #
-# #
-##########################################################################
-
-all: generate
- ./generate --help
-
-
-generate: lexer.mll html_generator.ml
- ocamllex -o lexer.ml lexer.mll
- ocamlc -g -o generate lexer.ml html_generator.ml
-
-html: generate
- ./generate ../../Changelog -html /usr/local/shared/changelog -o Changelog.html
-
-clean:
- rm generate lexer.cmi lexer.cmx lexer.o lexer.ml html_generator.cmi html_generator.cmx html_generator.o
-
-CSS= template.css content.css dev16-break.png user16.png \
- bug-break.png dev16.png private.png warning.png \
- bugfix.png user16-break.png
-
-install:
- cp generate /usr/local/bin/changelog
- mkdir -p /usr/local/shared/changelog
- for file in $(CSS) ; \
- do svn export "https://svn.frama-c.com/frama-c/distrib/modern/$$file" /usr/local/shared/changelog/$$file ; \
- done
-
-uninstall:
- rm -f /usr/local/bin/changelog
- rm -fr /usr/local/shared/changelog
diff --git a/doc/changelog/README b/doc/changelog/README
deleted file mode 100644
index 16ed22d8158c79a718150b05987bcf6ece27744b..0000000000000000000000000000000000000000
--- a/doc/changelog/README
+++ /dev/null
@@ -1,58 +0,0 @@
-----------------------------------------------------
---- Changelog Generator
-----------------------------------------------------
-
-Tool used by the doc/www/src/Makefile
-
-----------------------------------------------------
-Syntax of changelog entries :
-----------------------------------------------------
-
-# Mark "*": bug fixed.
-# Mark "-": change with an impact for users.
-# Mark "o": change with an impact for developers only.
-# Mark "!": change that can break compatibility with existing development.
-# '#nnn' : BTS entry #nnn
-# '#!nnn' : BTS private entry #nnn
-# '#?nnn' : OLD-BTS entry #nnn
-
-----------------------------------------------------
-Syntax of Frama-C release:
-----------------------------------------------------
-
-######################################################
-Open Source Release <FRAMAC-NAME>_<FRAMAC_VERSION>
-######################################################
-
-----------------------------------------------------
-Syntax of Frama-C external plugin release:
-----------------------------------------------------
-
-###################################
-Plugin <Name> <Version> <FRAMAC-NAME>_<FRAMAC_VERSION>
-###################################
-
-or (to refers to the current kernel version of Frama-C):
-###################################
-Plugin <Name> <Version>
-###################################
-
-----------------------------------------------------
-Syntax tool release:
-----------------------------------------------------
-
-###################################
-Tool <Name> <Version>
-###################################
-
-----------------------------------------------------
-Name of services for external plugins:
-----------------------------------------------------
-# Cmd : command line interface
-# Gui : graphical user interface
-# <Plugin> : plugin general
-# <Service> : plugin sub-service
-
-
-
-
diff --git a/doc/changelog/html_generator.ml b/doc/changelog/html_generator.ml
deleted file mode 100644
index 9e7754b5bb39786ef61a3bdd729b512503e9383f..0000000000000000000000000000000000000000
--- a/doc/changelog/html_generator.ml
+++ /dev/null
@@ -1,377 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2016 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* All rights reserved. *)
-(* Contact CEA LIST for licensing. *)
-(* *)
-(**************************************************************************)
-
-open Lexer
-
-let html = ref None
-let output = ref "Changelog.prehtml"
-let set_output f = output := f
-let set_html l = html := Some l
-let set_plugin p = Lexer.plugin_mode := Some p
-
-(* -------------------------------------------------------------------------- *)
-(* --- Main HTML --- *)
-(* -------------------------------------------------------------------------- *)
-
-let print_css fmt =
- begin
- Format.fprintf fmt
- "<style type=\"text/css\">\n\
- #legend div { float:right; margin:0pt; background-color: red; }\n\
- #legend ul { margin:0pt; }\n\
- #legend li { margin:0pt; }\n\
- li { font-size:10pt; margin-top:0pt; margin-bottom:0pt; }\n" ;
- let link = match !html with Some link -> link | None -> "<#relative-path-to-web-site>modern" in
- List.iter
- (fun (sty,icon) ->
- Format.fprintf fmt " .%-10s { list-style-image:url(\"%s/%s\"); }\n" sty link icon
- ) [ "user" , "user16.png" ;
- "user-break" , "user16-break.png" ;
- "dev" , "dev16.png" ;
- "dev-break" , "dev16-break.png" ;
- "bugfix" , "bugfix.png" ;
- "bug-break" , "bug-break.png" ;
- "lock" , "private.png" ;
- "warn" , "warning.png" ;
- ] ;
- Format.fprintf fmt
- " a.private { background-image:url(\"%s/private.png\"); \n\
- background-repeat: no-repeat;\n\
- background-position: left;\n\
- padding-left:10pt; }\n\
- h1.release { background-color:#F0F0F0; border:none; padding-bottom:3pt; }\n\
- .hversion { margin-left:1em; font-family: \"Courier\", monospace; font-size:0.7em; color:#808080; }\n\
- .kernel { font-family: \"Courier\", monospace; font-size:0.8em; color: #808080; }\n\
- </style>\n" link ;
- end
-
-let print_legend fmt =
- let print_icons fmt xs =
- Format.fprintf fmt "<ul>\n" ;
- List.iter
- (fun (icon,descr) -> Format.fprintf fmt "<li class=\"%s\">%s</li>\n" icon descr)
- xs ;
- Format.fprintf fmt "</ul>" ;
- in
- Format.fprintf fmt "<center><table id=\"legend\" summary=\"legend\"><tr valign=\"top\"><td>%a</td><td>%a</td></tr></table></center>@."
- print_icons [
- "user" , "new feature" ;
- "bugfix" , "bug fix" ;
- "dev" , "plug-in developers" ;
- ]
- print_icons [
- "warn" , "compatibility break" ;
- "lock" , "private bts entries" ;
- ]
-
-let print_head fmt =
- match !html with
- | Some link ->
- begin
- Format.fprintf fmt "<html>@\n<head>\n\
- <link rel=\"stylesheet\" href=\"%s/template.css\" type=\"text/css\" />\n\
- <link rel=\"stylesheet\" href=\"%s/content.css\" type=\"text/css\" />\n"
- link link ;
- print_css fmt ;
- Format.fprintf fmt "</head>\n<body><div id=\"content\">\n" ;
- end
- | None ->
- begin
- Format.fprintf fmt "<#def header-hook>\n" ;
- print_css fmt ;
- Format.fprintf fmt "</#def>\n<#head>\n" ;
- end
-
-let print_title fmt =
- match !plugin_mode with
- | None ->
- Format.fprintf fmt "<h1>Changes in Frama-C by Release</h1>\n"
- | Some p ->
- Format.fprintf fmt "<h1>Changes in Frama-C %s by Release</h1>\n" p
-
-let print_trail fmt =
- if !html <> None then Format.fprintf fmt "</div></body>\n</html>@."
- else Format.fprintf fmt "<#foot>@."
-
-let print_text fmt s =
- for i=0 to String.length s - 1 do
- match s.[i] with
- | '&' -> Format.pp_print_string fmt "&"
- | '"' -> Format.pp_print_string fmt """
- | ' ' -> Format.pp_print_string fmt " "
- | '>' -> Format.pp_print_string fmt ">"
- | '<' -> Format.pp_print_string fmt "<"
- | c -> Format.pp_print_char fmt c
- done
-
-(* -------------------------------------------------------------------------- *)
-(* --- Entries --- *)
-(* -------------------------------------------------------------------------- *)
-
-let print_word fmt = function
- | Space -> Format.pp_print_char fmt ' '
- | Newline -> Format.pp_print_string fmt "<br/><br/>"
- | Word s -> print_text fmt s
- | Quoted s -> Format.fprintf fmt "<tt>%a</tt>" print_text s
- | Item k -> Format.fprintf fmt "<br/><i>%c</i>. " k
- | PublicBts n ->
- Format.fprintf fmt "<a class=\"public\" href=\"%s%d\">#%d</a>"
- "http://bts.frama-c.com/view.php?id=" n n
- | PrivateBts n ->
- Format.fprintf fmt "<a class=\"private\" href=\"%s%d\">#%d</a>"
- "http://bts.frama-c.com/view.php?id=" n n
- | Gitlab n ->
- Format.fprintf fmt "<a class=\"private\" href=\"%s%d\">#%d</a>"
- "https://git.frama-c.com/frama-c/frama-c/issues/" n n
- | OldBts n ->
- Format.fprintf fmt "<tt>'%d'</tt>" n
-
-type category =
- | UserFeature
- | UserBugfix
- | DeveloperTopics
-
-let category e =
- if List.mem Developer e.tags then DeveloperTopics
- else
- if List.mem Bugfix e.tags
- then UserBugfix
- else UserFeature
-
-let category_compare k1 k2 =
- let rank = function
- | UserFeature -> 1
- | UserBugfix -> 2
- | DeveloperTopics -> 3
- in
- rank k1 - rank k2
-
-let category_title n = function
- | UserFeature -> if n > 1 then "New Features" else "New Feature"
- | UserBugfix -> if n > 1 then "Bug Fixes" else "Bug Fix"
- | DeveloperTopics -> "Developers Only"
-
-let print_service fmt = function
- | Main | Plugin(_,None) -> ()
- | Cmd -> Format.fprintf fmt "<span class=\"kernel\">[Cmd]</span> "
- | Gui -> Format.fprintf fmt "<span class=\"kernel\">[Gui]</span> "
- | Service s | Plugin(_,Some s) -> Format.fprintf fmt "<span class=\"kernel\">[%s]</span> " s
-
-let print_entry fmt e =
- let kind =
- let break = List.mem Break e.tags in
- match category e with
- | UserFeature -> if break then "user-break" else "user"
- | UserBugfix -> if break then "bug-break" else "bugfix"
- | DeveloperTopics -> if break then "dev-break" else "dev"
- in
- Format.fprintf fmt "<li class=\"%s\">" kind ;
- print_service fmt e.service ;
- List.iter (print_word fmt) (List.rev e.descr) ;
- Format.fprintf fmt "</li>@\n"
-
-(* -------------------------------------------------------------------------- *)
-(* --- Entries --- *)
-(* -------------------------------------------------------------------------- *)
-
-let by_service e1 e2 = service_compare e1.service e2.service
-let by_category e1 e2 = category_compare (category e1) (category e2)
-let by_break e1 e2 =
- match List.mem Break e1.tags , List.mem Break e2.tags with
- | true , false -> 1
- | false , true -> -1
- | _ -> 0
-
-let compare_entry e1 e2 =
- let rec cmp x y = function
- | [] -> 0
- | f :: fs ->
- let c = f x y in
- if c=0 then cmp x y fs
- else c
- in
- cmp e1 e2 [by_service;by_category;by_break]
-
-let print_entries fmt es =
- begin
- Format.fprintf fmt "<ul class=\"entries\">@\n" ;
- List.iter (print_entry fmt) (List.sort compare_entry es) ;
- Format.fprintf fmt "</ul>@." ;
- end
-
-let print_category_entries fmt (c,es) =
- let n = List.length es in
- if n > 0 then
- begin
- Format.fprintf fmt "<h3>%s</h3>@\n" (category_title n c) ;
- print_entries fmt es ;
- end
-
-let sort_by f cmp es =
- let es = List.sort (fun e1 e2 -> cmp (f e2) (f e1)) es in
- let rec acc sorted item content = function
- | [] -> (item,content) :: sorted
- | e :: es ->
- let k = f e in
- if cmp k item = 0
- then acc sorted item (e::content) es
- else acc ((item,content)::sorted) k [e] es
- in match es with
- | [] -> []
- | e::es -> acc [] (f e) [e] es
-
-let print_entries fmt es =
- if List.length es >= 5 then
- match sort_by category category_compare es with
- | [_,es] -> print_entries fmt es
- | ces ->
- if List.exists (fun (_,es) -> List.length es > 2) ces
- then List.iter (print_category_entries fmt) ces
- else print_entries fmt es
- else
- print_entries fmt es
-
-(* -------------------------------------------------------------------------- *)
-(* --- Entries by Service --- *)
-(* -------------------------------------------------------------------------- *)
-
-module Title = struct type t = string let compare = compare_string end
-module Smap = Map.Make(Title)
-
-type sections = {
- mutable s_main : entry list ;
- mutable s_cmd : entry list ;
- mutable s_gui : entry list ;
- mutable s_plugin : entry list Smap.t ;
- mutable s_service : entry list Smap.t ;
-}
-
-let sections () = {
- s_main = [] ;
- s_cmd = [] ;
- s_gui = [] ;
- s_plugin = Smap.empty ;
- s_service = Smap.empty ;
-}
-
-let smap_add (a:string) (e:entry) (s:entry list Smap.t) =
- let es = try Smap.find a s with Not_found -> [] in
- Smap.add a (e::es) s
-
-let framac_sections s e =
- match e.service with
- | Main | Cmd -> s.s_main <- e :: s.s_main
- | Gui -> s.s_gui <- e :: s.s_gui
- | Plugin(p,_) -> s.s_plugin <- smap_add p e s.s_plugin
- | Service _ -> s.s_main <- e :: s.s_main
-
-let plugin_sections s e =
- match e.service with
- | Main -> s.s_main <- e :: s.s_main
- | Cmd -> s.s_cmd <- e :: s.s_cmd
- | Gui -> s.s_gui <- e :: s.s_gui
- | Plugin(p,_) -> s.s_plugin <- smap_add p e s.s_plugin
- | Service a -> s.s_service <- smap_add a e s.s_service
-
-
-let print_sections fmt es =
- let s = sections () in
- let entity,dispatch = match !plugin_mode with
- | None -> "Frama-C" , framac_sections
- | Some p -> p , plugin_sections
- in
- begin
- List.iter (dispatch s) es ;
- if s.s_main <> [] then
- ( Format.fprintf fmt "<h2>%s General</h2>@\n" entity ;
- print_entries fmt s.s_main ) ;
- if s.s_cmd <> [] then
- ( Format.fprintf fmt "<h2>%s Command Line</h2>@\n" entity ;
- print_entries fmt s.s_cmd ) ;
- if s.s_gui <> [] then
- ( Format.fprintf fmt "<h2>%s GUI</h2>@\n" entity ;
- print_entries fmt s.s_gui ) ;
- Smap.iter
- (fun s es ->
- Format.fprintf fmt "<h2>%s - %s</h2>@\n" entity s ;
- print_entries fmt es )
- s.s_service ;
- Smap.iter
- (fun p es ->
- Format.fprintf fmt "<h2>Plugin %s</h2>@\n" p ;
- print_entries fmt es )
- s.s_plugin ;
- end
-
-(* -------------------------------------------------------------------------- *)
-(* --- Release Printing --- *)
-(* -------------------------------------------------------------------------- *)
-
-let print_release fmt = function
- | Current ->
- Format.fprintf fmt
- "<h1 class=\"release\">Future Release <span class=\"hversion\">[svn]</span></h1>@\n"
- | Release(a,v) ->
- Format.fprintf fmt
- "<div><a id=\"%s-%s\" href=\"#%s-%s\"></a><p> </p><p> </p><p> </p><p> </p></div>\
- <h1 class=\"release\">%s Release <span class=\"hversion\">[%s]</span></h1>@ \n"
- a v a v a v
- | ToolRelease(a,v) ->
- Format.fprintf fmt
- "<div><a id=\"%s-%s\" href=\"#%s-%s\"></a><p> </p><p> </p><p> </p><p> </p></div>\
- <h1 class=\"release\">Release %s %s</h1>@ \n"
- a v a v a v
- | CurrentPlugin(a,v) ->
- Format.fprintf fmt
- "<div><a id=\"%s-%s\" href=\"#%s-%s\"></a><p> </p><p> </p><p> </p><p> </p></div>\
- <h1 class=\"release\">Future Release %s %s</h1>@ \n"
- a v a v a v
- | PluginRelease(a,v,kernel,framac) ->
- Format.fprintf fmt
- "<div><a id=\"%s-%s\" href=\"#%s-%s\"></a><p> </p><p> </p><p> </p><p> </p></div>\
- <h1 class=\"release\">Release %s %s<span class=\"hversion\">[%s %s]</span></h1>@ \n"
- a v a v a v kernel framac
-
-let print_releases fmt releases =
- List.iter
- (fun (release, entries) ->
- if entries <> [] then
- begin
- print_release fmt release ;
- Format.fprintf fmt "<div class=\"release\">@." ;
- print_sections fmt entries ;
- Format.fprintf fmt "</div>@." ;
- end)
- (Lexer.releases ())
-
-(* -------------------------------------------------------------------------- *)
-(* --- HTML Generation & Command Line --- *)
-(* -------------------------------------------------------------------------- *)
-
-let generate () =
- let cout = open_out !output in
- let fmt = Format.formatter_of_out_channel cout in
- print_head fmt ;
- print_title fmt ;
- print_legend fmt ;
- print_releases fmt releases ;
- print_trail fmt
-
-let () =
- Arg.parse [
- "-html" , Arg.String set_html , "<css> generate html (resources directory <css>)" ;
- "-plugin" , Arg.String set_plugin , "<name> generate changelog for plugin" ;
- "-o" , Arg.String set_output , "<file> output file" ;
- ] Lexer.process "changelog [options] files..." ;
- generate ()
-
diff --git a/doc/changelog/lexer.mll b/doc/changelog/lexer.mll
deleted file mode 100644
index 37147a667fa838bd0ffc23cf0cbd9ec5d1e45c27..0000000000000000000000000000000000000000
--- a/doc/changelog/lexer.mll
+++ /dev/null
@@ -1,285 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2016 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* All rights reserved. *)
-(* Contact CEA LIST for licensing. *)
-(* *)
-(**************************************************************************)
-
-{
-
- type release =
- | Current
- | Release of string * string
- | CurrentPlugin of string * string
- (* plugin-name, plugin-version *)
- | PluginRelease of string * string * string * string
- (* plugin-name, plugin-version, kernel-name, kernel-version *)
- | ToolRelease of string * string
- (* tool-name, tool-version *)
-
- type service =
- | Cmd
- | Main
- | Gui
- | Plugin of string * string option
- | Service of string
-
- type tag = Break | Bugfix | User | Developer | Commits
-
- type text =
- | Word of string
- | Quoted of string
- | PublicBts of int
- | PrivateBts of int
- | OldBts of int
- | Gitlab of int
- | Item of char
- | Space
- | Newline
-
- type entry = {
- mutable service: service;
- mutable tags: tag list;
- mutable descr: text list;
- }
-
- let plugin_mode : string option ref = ref None
- let current_plugin = ref None
- let framac_services = [
- "Cil";
- "Configure";
- "Journal";
- "Kernel";
- "Logic";
- "Makefile";
- "Project";
- ]
-
- let releases : (release * entry list) list ref = ref [ Current, [] ]
-
- let file = ref "Changelog"
- let line = ref 1
-
- let error msg =
- Format.eprintf "%s:%d: " !file !line;
- Format.kfprintf
- (fun fmt ->
- Format.pp_print_newline fmt () ;
- exit 2)
- Format.err_formatter msg
-
- let set_release cp r =
- let entries = try List.assoc r !releases with Not_found -> [] in
- let others = List.filter (fun (r',_) -> r<>r') !releases in
- current_plugin := cp ;
- releases := (r, entries) :: others
-
- let add_entry e = function
- | ( r , es ) :: olders -> ( r , e::es ) :: olders
- | _ -> assert false
-
- let set_name e a =
- e.service <-
- match !plugin_mode , !current_plugin , a with
- | None , None , ("Cmd"|"CMD") -> Cmd
- | None , None , ("Gui"|"GUI") -> Gui
- | None , None , _ -> if List.mem a framac_services then Service a else Plugin(a,None)
- | None , Some p , ("Cmd"|"CMD") -> Plugin(p,Some "Cmd")
- | None , Some p , ("Gui"|"GUI") -> Plugin(p,Some "GUI")
- | None , Some p , s -> Plugin(p,Some s)
- | Some _ , None , s -> Service s
- | Some _ , Some p , s ->
- if (String.uppercase p)=(String.uppercase s) then Main else Service a
-
- let set_tag e t = e.tags <- t :: e.tags
-
- let mk_entry mark =
- let entry = { service = Main; tags = []; descr = [] } in
- String.iter
- (function
- | '-' -> set_tag entry User
- | 'o' -> set_tag entry Developer
- | '*' -> set_tag entry Bugfix
- | '!' -> set_tag entry Break
- | '+' -> set_tag entry Commits
- | _ -> ())
- mark ;
- releases := add_entry entry !releases ;
- entry
-
- let add_word e w = match e.descr , w with
- | Space :: _ , Space -> ()
- | d , _ -> e.descr <- w :: d
-
-}
-
-let space = [' ' '\t']
-let newline = ['\n' '\r']+
-let upper = ['A'-'Z']
-let letter = ['a'-'z' 'A'-'Z' '_']
-let ident = ['a'-'z' 'A'-'Z' '_' '0'-'9']
-let file = ['a'-'z' 'A'-'Z' '_' '-' '0'-'9']
-let digit = ['0'-'9']
-let word = [^ ' ' '\t' '\n' '\r']
-let mark = ['-' 'o' '*' '!' '+']
-
-let vdigit = [ '0'-'9' '.' ]
-
-(* ce is the current entry. None means no-entry at the beginning of line. *)
-rule main ce = parse
- | (mark+) as mark { entry (mk_entry mark) lexbuf }
- | '#' [^ '\n']* '\n' { incr line; main None lexbuf }
- | newline { incr line; main None lexbuf }
- | eof { }
- | ( letter+ space+ )* ( (letter+) as name ) '-' ((digit+) as version)
- { set_release None (Release(name,version)) ;
- main None lexbuf }
- | space* "Tool" space+
- ( (ident+) as name ) space+
- ( (vdigit+) as version) space*
- { let r = ToolRelease(name,version) in
- set_release None r ; main None lexbuf }
- | space* "Plugin" space+
- ( (ident+) as name ) space+
- ( (vdigit+) as version) space*
- newline
- { incr line;
- begin
- match !plugin_mode with
- | Some _ ->
- let r = CurrentPlugin(name,version) in
- set_release None r
- | None ->
- set_release (Some name) Current
- end;
- main None lexbuf }
- | space* "Plugin" space+
- ( (ident+) as name ) space+
- ( (vdigit+) as version) space+
- ( (letter+) as framac) '_' ((digit+) as kernel)
- { begin
- match !plugin_mode with
- | Some _ ->
- let r = PluginRelease(name,version,framac,kernel) in
- set_release None r
- | None ->
- let r = Release(framac,kernel) in
- set_release (Some name) r
- end;
- main None lexbuf }
- | space
- {
- match ce with
- | None -> main ce lexbuf
- | Some e -> text e lexbuf
- }
- | _
- {
- error "Misformed entry (%S)" (Lexing.lexeme lexbuf)
- }
-
-(* e is just created *)
-and entry e = parse
- | space { entry e lexbuf }
- | (letter+) as a { set_name e a ; text e lexbuf }
- | _ { error "Missing plugin or service name (at %S)" (Lexing.lexeme lexbuf) }
-
-(* text of entry *)
-and text e = parse
- | '[' digit + '/' digit+ ('/' digit+)? ']' { (* date *) text e lexbuf }
- | newline newline { incr line ; add_word e Newline ; main (Some e) lexbuf }
- | newline { incr line ; main (Some e) lexbuf }
- | space { add_word e Space ; text e lexbuf }
- | eof { }
-
- | space+ (digit as k) ')' { add_word e (Item k) ; text e lexbuf }
-
- | '#' ((digit+) as bug)
- { add_word e (PublicBts(int_of_string bug)) ; text e lexbuf }
-
- | "#!" ((digit+) as bug)
- { add_word e (PrivateBts(int_of_string bug)) ; text e lexbuf }
-
- | "#?" ((digit+) as bug)
- { add_word e (OldBts(int_of_string bug)) ; text e lexbuf }
-
- | "#@" ((digit+) as bug)
- { add_word e (Gitlab(int_of_string bug)) ; text e lexbuf }
-
- | '-' (letter | '-')+
- | '!'? (upper ident* '.')+ ident+
- | '~' ident+
- | '"' [^ '"' '\n']* '"'
- | ( (file+ | '.' | "..") '/' ) * file+ '.' file+
- | ( (file+ | '.' | "..") '/' ) + file+ '/'?
- | '\\' ident+
- { add_word e (Quoted(Lexing.lexeme lexbuf)) ; text e lexbuf }
- | letter+ ('-' letter+)*
- { add_word e (Word (Lexing.lexeme lexbuf)) ; text e lexbuf }
-
- | _ { add_word e (Word (Lexing.lexeme lexbuf)) ; text e lexbuf }
-
-{
-
- let process filename =
- let cin = open_in filename in
- let lexbuf = Lexing.from_channel cin in
- file := filename ;
- line := 1 ;
- main None lexbuf
-
- let compare_string s1 s2 =
- let cmp = String.compare (String.uppercase s1) (String.uppercase s2) in
- if cmp = 0 then String.compare s1 s2 else cmp
-
- let rec compare_strings s1 s2 =
- match s1 , s2 with
- | [] , _ -> (-1)
- | _ , [] -> 1
- | x::s1 , y::s2 ->
- let cmp = compare_string x y in
- if cmp = 0 then compare_strings s1 s2 else cmp
-
- let service_compare s1 s2 =
- let rank = function
- | Main -> (0,[])
- | Cmd -> (1,[])
- | Gui -> (2,[])
- | Service a -> (3,[a])
- | Plugin(p,None) -> (4,[p])
- | Plugin(p,Some a) -> (4,[p;a])
- in
- let (r1,a1) = rank s1 in
- let (r2,a2) = rank s2 in
- if r1=r2 then compare_strings a1 a2 else r1-r2
-
- let compare_release (r1,_) (r2,_) =
- match r1 , r2 with
- | Current , Current -> 0
- | Current , _ -> -1
- | _ , Current -> 1
- | CurrentPlugin (_,v1), CurrentPlugin (_,v2) -> String.compare v2 v1
- | CurrentPlugin _, _ -> -1
- | _ , CurrentPlugin _-> 1
- | Release(_,v1) , Release(_,v2) -> String.compare v2 v1
- | Release _ , _ -> -1
- | _ , Release _ -> 1
- | PluginRelease(_,v1,_,a1) , PluginRelease(_,v2,_,a2) ->
- String.compare (a2 ^ v2) (a1 ^ v1)
- | PluginRelease _ , _ -> -1
- | _, PluginRelease _ -> 1
- | ToolRelease(_,v1) , ToolRelease(_,v2) ->
- String.compare v2 v1
-
- let releases () =
- List.map
- (fun (r,es) -> r , List.filter (fun e -> not (List.mem Commits e.tags)) es)
- (List.sort compare_release !releases)
-
-}
diff --git a/doc/developer/changes.tex b/doc/developer/changes.tex
index c8b8b83c07618fced8fcce85064bed1eb8a9351b..7e5d6609178d092bdd6263edcabec0a9ce549806 100644
--- a/doc/developer/changes.tex
+++ b/doc/developer/changes.tex
@@ -7,8 +7,10 @@ This chapter summarizes the major changes in this documentation between each
\section*{\framacversion}
+\section*{Silicon-20161101}
+
\begin{itemize}
-\item\textbf{ACSL Extensions}: Update documentation for newly
+\item\textbf{ACSL Extensions}: Updated documentation for newly
introduced loop extensions.
\end{itemize}
diff --git a/doc/developer/developer.tex b/doc/developer/developer.tex
index c02bcba52fe18c3620201d945b1753d12450830a..2b09445a3105d82cc72ae01f48b27ec5af72a575 100644
--- a/doc/developer/developer.tex
+++ b/doc/developer/developer.tex
@@ -42,7 +42,7 @@ CEA LIST, Software Security Laboratory, Saclay,F-91191
\end{center}
\vfill
\begin{flushleft}
- \textcopyright 2009-2016 CEA LIST
+ \textcopyright 2009-{\the\year} CEA LIST
\end{flushleft}
\end{titlepage}
diff --git a/doc/frama-c-book.cls b/doc/frama-c-book.cls
index 01090add59fe2cde8650632031cd210c718e49d3..ce737a78d1aa6e6c2bca8ebd3c458306e872d521 100644
--- a/doc/frama-c-book.cls
+++ b/doc/frama-c-book.cls
@@ -109,7 +109,7 @@
\titleformat{\chapter}[display]{\Huge\raggedleft}%
{\huge\chaptertitlename\,\thechapter}{0.5em}{}
\titleformat{\section}[hang]{\Large\bfseries}{\thesection}{1em}{}%
-[\vspace{-14pt}\rule{\textwidth}{0.1pt}\vspace{-8pt}]
+[\vspace{-14pt}\rule{\textwidth}{0.1pt}\nopagebreak\vspace{-8pt}]
\titleformat{\subsubsection}[hang]{\bfseries}{}{}{}%
[\vspace{-8pt}]
diff --git a/doc/release/build.tex b/doc/release/build.tex
index 37ad5312bd1a70b85175682dc5e93a60cae6ea01..e5de21e0c3a515018c15675e98e6006321d62c91 100644
--- a/doc/release/build.tex
+++ b/doc/release/build.tex
@@ -34,8 +34,11 @@ There are many administrative steps, coordinated by the release manager.
\begin{enumerate}
\item Set \texttt{VERSION} file.
\item Update file \texttt{ALL\_VERSIONS}. \todo{Cannot be done with RC releases. Must be put somewhere else in the file}
-\item Update file \texttt{Changelog}, as well as \texttt{src/plugins/wp/Changelog}, to
- add the header corresponding to the new version.
+\item Update file \texttt{Changelog}, as well as
+ \texttt{src/plugins/wp/Changelog}, to add the header corresponding to the
+ new version. % For the final release, use the script
+ % \texttt{doc/changelog/generate} to check that the HTML page can be built,
+ % and check its contents.
\item Update the Frama-C's authors list in files
\texttt{src/plugins/gui/help\_manager.ml} and \texttt{opam/opam}.
\item Recompile and test to check that all is fine.
@@ -54,10 +57,6 @@ Generated documents from the \texttt{trunk} generally take into account the
changes that have happened, divided by version of Frama-C. Make sure that the
first section has the correct release name.
-\todo{Check that all manuals use VERSION.}
-
-\todo{Migrate all manuals to use \texttt{\textbackslash the\textbackslash year}. for the Copyright year}
-
\todo{Mention the other things that change from one release to the
other, such as the ACSL version number}
@@ -80,9 +79,9 @@ file:
\textsf{ACSL Implementation} &
\texttt{doc/speclang} &
\expertise{Virgile} \\
- \textsf{man page} &
- \texttt{man/frama-c.1} &
- \expertise{Virgile} \\
+ % \textsf{man page} &
+ % \texttt{man/frama-c.1} &
+ % \expertise{Virgile} \\
\hline
\end{tabular}
\end{center}
@@ -111,6 +110,11 @@ isn't exhaustive:
\end{tabular}
\end{center}
+Clone the \texttt{acsl} manual
+(\url{git@github.com:acsl-language/acsl.git}) in
+\texttt{doc/acsl} in order to generate the ACSL reference and implementation
+manuals.
+
Clone the \texttt{manuals} repository
(\url{git@git.frama-c.com:frama-c/manuals.git}) in
\texttt{doc/manuals} in order to update the manuals (required by the
@@ -176,8 +180,8 @@ copy them to the website. It also copies the manuals.
\expertise{release manager} Use the script
\texttt{build-src-distrib.sh} for this purpose (\texttt{bash version
4} required) after cloning the repository
-\texttt{website}(\texttt{git@git.frama-c.com:frama-c/website}) in
-directory \texttt{website}. You can create a specific branch in this
+\texttt{website} (\texttt{git@git.frama-c.com:frama-c/website}) in
+the root directory of Frama-C. You can create a specific branch in this
repository in order to later do the merge request.
If you have problem with UTF-8 encoded filenames:
diff --git a/doc/release/release.tex b/doc/release/release.tex
index 2a0b6f49a348e306ce6e9d7ceb06d6a9520707ea..d24374a6132744b01d8bb4e02ee9fe1d763cfdce 100644
--- a/doc/release/release.tex
+++ b/doc/release/release.tex
@@ -18,7 +18,6 @@
\input{intro}
\input{branch}
\input{build}
-
\input{website}
\end{document}
diff --git a/doc/release/website.tex b/doc/release/website.tex
index a6cdcd8702c21de3620660312dde337eae4cd9b8..8378cab595b739d0f65b728378de708dfac3b4c0 100644
--- a/doc/release/website.tex
+++ b/doc/release/website.tex
@@ -1,4 +1,4 @@
-\chapter{The Distribution Stage}
+\chapter{The Website Stage}
Where all our efforts goes on the web. There are two very different
tasks for \FramaC to go online. Authoring the web site pages is the
@@ -6,10 +6,15 @@ responsibility of the developpers and the release manager. Publishing
the web site can only be performed by authorized peoples, who may not
be the release manager.
+\section{Requirements}
+
+You need \texttt{pandoc} and \texttt{tidy} to perform those steps.
+They can be installed from your Linux distribution.
+
\section{Authoring the Pages}
To edit the web pages of the site, developpers only need the
\texttt{trunk} branch of the repository. The web site sources are in
-\texttt{doc/www/src}.
+\texttt{src} or the checkout of the \texttt{website} tree.
\subsection{Editing Web Pages}
@@ -21,8 +26,9 @@ Compile the web pages with:
\$ make local
\end{shell}
-Here, you get a snapshot of the web-site in \texttt{doc/www/src},
-without any downlable resources.
+This way, you get a snapshot of the web-site in \texttt{src},
+without any downloadable resources. You can start browsing at
+\texttt{index.html}
\subsection{Adding News}
The news are defined in the \texttt{news.def} page. All the news
@@ -75,17 +81,16 @@ The current (\emph{awkward}) procedure is as follows:
You should at least update the links to reference documentation from the
\texttt{support.prehtml} page.
\end{enumerate}
-\item Add the page \texttt{install-NAME} where \texttt{NAME} is the version
- name of the distribution (diff the file \texttt{INSTALL} of the previous
- release with \texttt{TRUNK/INSTALL} and update \texttt{install-PREVIOUS-NAME}
- accordingly).
+\item Copy the file \texttt{INSTALL.md} from Frama-C to
+ \texttt{INSTALL-NAME.md} where \texttt{NAME} is the version name of the
+ distribution.
\item Build the web site:
\begin{shell}[gobble=4]
\$ make local
\$ make distrib
\end{shell}
- You get a snap-shot of the repository in the newly created
- \texttt{doc/www/distrib} directory. Test it carefully.\\
+ You get a snap-shot of the repository in the \texttt{www} directory.
+ Test it carefully.\\
Automatic testing for compliance to \textsf{W3C} and links consistency
was launched (install the required tools before if necessary).
diff --git a/doc/rte/macros_modern.tex b/doc/rte/macros_modern.tex
new file mode 100644
index 0000000000000000000000000000000000000000..d5495a850c8dfe42bd5f3e32fcb96cd5ba53aa66
--- /dev/null
+++ b/doc/rte/macros_modern.tex
@@ -0,0 +1,174 @@
+%%% Environnements dont le corps est suprimé, et
+%%% commandes dont la définition est vide,
+%%% lorsque PrintRemarks=false
+
+\usepackage{comment}
+
+% true = prints marks signaling the state of the implementation
+% false = prints only the ACSL definition, without remarks on implementation.
+\newboolean{PrintImplementationRq}
+\setboolean{PrintImplementationRq}{true}
+
+% true = remarks about the current state of implementation in Frama-C
+% are in color.
+% false = they are rendered with an underline
+\newboolean{ColorImplementationRq}
+\setboolean{ColorImplementationRq}{true}
+
+%%% Commandes et environnements pour la version relative à l'implementation
+\newcommand{\highlightnotimplemented}{%
+\ifthenelse{\boolean{ColorImplementationRq}}{\color{red}}%
+ {\ul}%
+}%
+
+\newcommand{\notimplemented}[2][]{%
+\ifthenelse{\boolean{PrintImplementationRq}}{%
+ \begin{changebar}%
+ {\highlightnotimplemented #2}%
+ \ifthenelse{\equal{#1}{}}{}{\footnote{#1}}%
+ \end{changebar}%
+}%
+{#2}}
+
+\newenvironment{notimplementedenv}[1][]{%
+\ifthenelse{\boolean{PrintImplementationRq}}{%
+ \begin{changebar}%
+ \highlightnotimplemented%
+ \ifthenelse{\equal{#1}{}}{}{\def\myrq{#1}}%
+ \bgroup
+}{}}%
+{\ifthenelse{\boolean{PrintImplementationRq}}{%
+ \egroup%
+ \ifthenelse{\isundefined{\myrq}}{}{\footnote{\myrq}}\end{changebar}}{}}
+
+%%% Environnements et commandes non conditionnelles
+\newcommand{\experimental}{\textsc{Experimental}}
+
+
+\newsavebox{\fmbox}
+\newenvironment{cadre}
+ {\begin{lrbox}{\fmbox}\begin{minipage}{0.98\textwidth}}
+ {\end{minipage}\end{lrbox}\fbox{\usebox{\fmbox}}}
+
+
+\newcommand{\keyword}[1]{\lstinline|#1|\xspace}
+\newcommand{\keywordbs}[1]{\lstinline|\\#1|\xspace}
+
+\newcommand{\integer}{\keyword{integer}}
+\newcommand{\real}{\keyword{real}}
+\newcommand{\bool}{\keyword{boolean}}
+
+\newcommand{\Loop}{\keyword{loop}}
+\newcommand{\assert}{\keyword{assert}}
+\newcommand{\terminates}{\keyword{terminates}}
+\newcommand{\assume}{\keyword{assume}}
+\newcommand{\requires}{\keyword{requires}}
+\newcommand{\ensures}{\keyword{ensures}}
+\newcommand{\exits}{\keyword{exits}}
+\newcommand{\returns}{\keyword{returns}}
+\newcommand{\breaks}{\keyword{breaks}}
+\newcommand{\continues}{\keyword{continues}}
+\newcommand{\assumes}{\keyword{assumes}}
+\newcommand{\frees}{\keyword{frees}}
+\newcommand{\allocates}{\keyword{allocates}}
+\newcommand{\invariant}{\keyword{invariant}}
+\newcommand{\variant}{\keyword{variant}}
+\newcommand{\assigns}{\keyword{assigns}}
+\newcommand{\reads}{\keyword{reads}}
+\newcommand{\decreases}{\keyword{decreases}}
+
+\newcommand{\boundseparated}{\keywordbs{bound\_separated}}
+\newcommand{\Exists}{\keywordbs{exists}~}
+\newcommand{\Forall}{\keywordbs{forall}~}
+\newcommand{\bslambda}{\keywordbs{lambda}~}
+\newcommand{\fullseparated}{\keywordbs{full\_separated}}
+\newcommand{\distinct}{\keywordbs{distinct}}
+\newcommand{\Max}{\keyword{max}}
+\newcommand{\nothing}{\keywordbs{nothing}}
+\newcommand{\numof}{\keyword{num\_of}}
+\newcommand{\offsetmin}{\keywordbs{offset\_min}}
+\newcommand{\offsetmax}{\keywordbs{offset\_max}}
+\newcommand{\old}{\keywordbs{old}}
+\newcommand{\at}{\keywordbs{at}}
+
+\newcommand{\If}{\keyword{if}~}
+\newcommand{\Then}{~\keyword{then}~}
+\newcommand{\Else}{~\keyword{else}~}
+\newcommand{\For}{\keyword{for}~}
+\newcommand{\While}{~\keyword{while}~}
+\newcommand{\Do}{~\keyword{do}~}
+\newcommand{\Let}{\keywordbs{let}~}
+\newcommand{\Break}{\keyword{break}}
+\newcommand{\Return}{\keyword{return}}
+\newcommand{\Continue}{\keyword{continue}}
+
+\newcommand{\exit}{\keyword{exit}}
+\newcommand{\main}{\keyword{main}}
+\newcommand{\void}{\keyword{void}}
+
+\newcommand{\volatile}{\keyword{volatile}}
+\newcommand{\struct}{\keyword{struct}}
+\newcommand{\union}{\keywordbs{union}}
+\newcommand{\inter}{\keywordbs{inter}}
+\newcommand{\typedef}{\keyword{typedef}}
+\newcommand{\result}{\keywordbs{result}}
+\newcommand{\separated}{\keywordbs{separated}}
+\newcommand{\sizeof}{\keyword{sizeof}}
+\newcommand{\strlen}{\keywordbs{strlen}}
+\newcommand{\Sum}{\keyword{sum}}
+\newcommand{\valid}{\keywordbs{valid}}
+\newcommand{\validread}{\keywordbs{valid\_read}}
+\newcommand{\offset}{\keywordbs{offset}}
+\newcommand{\blocklength}{\keywordbs{block\_length}}
+\newcommand{\baseaddr}{\keywordbs{base\_addr}}
+\newcommand{\allocation}{\keywordbs{allocation}}
+\newcommand{\allocable}{\keywordbs{allocable}}
+\newcommand{\freeable}{\keywordbs{freeable}}
+\newcommand{\fresh}{\keywordbs{fresh}}
+\newcommand{\comparable}{\keywordbs{comparable}}
+
+\newcommand{\N}{\ensuremath{\mathbb{N}}}
+\newcommand{\ra}{\ensuremath{\rightarrow}}
+\newcommand{\la}{\ensuremath{\leftarrow}}
+
+
+% BNF grammar
+\newcommand{\indextt}[1]{\index{#1@\protect\keyword{#1}}}
+\newcommand{\indexttbs}[1]{\index{#1@\protect\keywordbs{#1}}}
+\newif\ifspace
+\newif\ifnewentry
+\newcommand{\addspace}{\ifspace ~ \spacefalse \fi}
+\newcommand{\term}[2]{\addspace\hbox{\lstinline|#1|%
+\ifthenelse{\equal{#2}{}}{}{\indexttbase{#2}{#1}}}\spacetrue}
+\newcommand{\nonterm}[2]{%
+ \ifthenelse{\equal{#2}{}}%
+ {\addspace\hbox{\textsl{#1}\ifnewentry\index{grammar entries!\textsl{#1}}\fi}\spacetrue}%
+ {\addspace\hbox{\textsl{#1}\footnote{#2}\ifnewentry\index{grammar entries!\textsl{#1}}\fi}\spacetrue}}
+\newcommand{\repetstar}{$^*$\spacetrue}
+\newcommand{\repetplus}{$^+$\spacetrue}
+\newcommand{\repetone}{$^?$\spacetrue}
+\newcommand{\lparen}{\addspace(}
+\newcommand{\rparen}{)}
+\newcommand{\orelse}{\addspace$\mid$\spacetrue}
+\newcommand{\sep}{ \\[2mm] \spacefalse\newentrytrue}
+\newcommand{\newl}{ \\ & & \spacefalse}
+\newcommand{\alt}{ \\ & $\mid$ & \spacefalse}
+\newcommand{\is}{ & $::=$ & \newentryfalse}
+\newenvironment{syntax}{\begin{tabular}{@{}rrll@{}}\spacefalse\newentrytrue}{\end{tabular}}
+\newcommand{\synt}[1]{$\spacefalse#1$}
+\newcommand{\emptystring}{$\epsilon$}
+\newcommand{\below}{See\; below}
+
+% colors
+
+\definecolor{darkgreen}{rgb}{0, 0.5, 0}
+
+% theorems
+
+\newtheorem{example}{Example}[chapter]
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-PDF-mode: t
+%%% TeX-master: "main"
+%%% End:
diff --git a/doc/rte/main.tex b/doc/rte/main.tex
index fbbfad74a63ca68478a7c8ffa2286704c1310fec..104500822c43736df870960bfad4f092f7b412a4 100644
--- a/doc/rte/main.tex
+++ b/doc/rte/main.tex
@@ -1,7 +1,7 @@
\documentclass[a4paper,11pt,twoside,openright,web]{frama-c-book}
%%\usepackage{microtype}
-\input{../speclang/macros_modern}
+\input{macros_modern}
%%\input{framacversion.tex}
%%modern \usepackage{pslatex}
%%modern \usepackage{a4wide}
@@ -64,7 +64,7 @@ CEA LIST, Software Safety Laboratory, Saclay, F-91191 \\
\end{tabular}
\vfill
\begin{flushleft}
- \textcopyright 2010-2016 CEA LIST
+ \textcopyright 2010-{\the\year} CEA LIST
\end{flushleft}
\end{titlepage}
diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index 52c21c876231010b81f40ad2124be722d544d346..cdaaa09cfc62c85c72511e6b912297f5db989e63 100644
--- a/doc/userman/user-changes.tex
+++ b/doc/userman/user-changes.tex
@@ -11,8 +11,11 @@ release. First we list changes of the last release.
\section*{\framacversion}
+\section*{Silicon-20161101}
+
\begin{itemize}
\item \textbf{Getting Started:} OCaml version greater or equal than 4.02.3 is required
+\item \textbf{Normalizing the Source Code:} New option \texttt{-c11}
\end{itemize}
\section*{Aluminium-20160501}
diff --git a/doc/userman/user-sources.tex b/doc/userman/user-sources.tex
index 8590324cfc85ceb4f365e857e73a323308ab352a..b6b9580b3fc31c40fc19cdc71d94314d6c8c8db0 100644
--- a/doc/userman/user-sources.tex
+++ b/doc/userman/user-sources.tex
@@ -253,6 +253,9 @@ To ignore this disabling \pragmadef{UNROLL} pragma and force unrolling, the opti
Passing a negative argument to \texttt{-ulevel} will disable unrolling, even
in case of \texttt{UNROLL} pragma.
+
+\item \optiondef{-}{c11} allows the use of some C11 constructs. Currently
+supported are typedefs redefinition.
\end{description}
\section{Predefined macros}\label{sec:predefined-macros}
diff --git a/doc/value/main.tex b/doc/value/main.tex
index 0ecafc795b2e8bd155f09f3fe1ca53eed558b118..917cf83126737e8d80a41f76dc644ff5030099de 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -41,15 +41,16 @@
%==============================================================================
\begin{document}
-\coverpage{Value Analysis}
+\coverpage{EVA - The Evolved Value Analysis plug-in}
\begin{titlepage}
\begin{flushleft}
\includegraphics[height=14mm]{cealistlogo.jpg}
\end{flushleft}
\vfill
-\title{Frama-C's value analysis plug-in}{\framacversion}
-\author{Pascal Cuoq and Boris Yakobowski with Matthieu Lemerre, André Maroneze,
+\title{The EVA plug-in}{\framacversion}
+\author{David Bühler, Pascal Cuoq and Boris Yakobowski. \\
+ With Matthieu Lemerre, André Maroneze,
Valentin Perrelle and Virgile Prevosto}
\begin{tabular}{l}
CEA LIST, Software Reliability Laboratory, Saclay, F-91191 \\
@@ -76,24 +77,24 @@ CEA LIST, Software Reliability Laboratory, Saclay, F-91191 \\
%\newpage
{\em Frama-C is a modular static analysis framework for the C language.\\
-This manual documents the value analysis plug-in of Frama-C.}
+This manual documents the EVA (for \emph{Evolved Value Analysis}) plug-in of Frama-C.}
\vspace{2cm}
-The value analysis plug-in automatically computes sets of possible
-values for the variables of an analyzed program. The value analysis
+The EVA plug-in automatically computes sets of possible
+values for the variables of an analyzed program. EVA
warns about possible run-time errors in the analyzed program.
Lastly, synthetic information
about each analyzed function can be computed automatically from the
-values provided by the value analysis: these functionalities (input
+values provided by EVA: these functionalities (input
variables, output variables, and information flow) are also documented
here. \bigskip
-The framework, the value analysis plug-in and the other plug-ins
+The framework, the EVA plug-in and the other plug-ins
documented here are all Open Source software. They can be
downloaded from \url{http://frama-c.com/}.
\bigskip
-In technical terms, the value analysis is context-sensitive and
+In technical terms, EVA is context-sensitive and
path-sensitive. In non-technical terms, this means that it tries to
offer precise results for a large set of C programs. Heterogeneous
pointer casts, function pointers, and floating-point computations are
@@ -103,7 +104,7 @@ handled.
Frama-C comes with two interfaces: batch and interactive.
The interactive graphical interface of Frama-C displays
a normalized version of the analyzed source code.
-In this interface, the value analysis plug-in allows the user
+In this interface, the EVA plug-in allows the user
to select an expression in the
code and observe an over-approximation of the set of
values this expression can take at run-time.
@@ -113,7 +114,7 @@ Here is a simple C example:
If either interface of Frama-C is launched with options
\lstinline|-val introduction.c|,
-the value analysis plug-in is able to guarantee that at each passage through
+the EVA plug-in is able to guarantee that at each passage through
the \lstinline|return| statement of
function \lstinline|f|, the global variables \lstinline+y+ and
\lstinline+z+ each contain either 1 or 3.
@@ -129,12 +130,12 @@ In an actual execution of this deterministic program,
there is only one passage though the end
of function \lstinline|main|, and therefore only one value for \lstinline|z|
at this point.
-The answer given by the value analysis is approximated but correct (the actual
+The answer given by EVA is approximated but correct (the actual
value, 3, is among the proposed values).
-The theoretical framework on which the value analysis is founded is called
+The theoretical framework on which EVA is founded is called
Abstract Interpretation and has been the subject of extensive research
-during the last fourty years.
+during the last forty years.
\section{Run-time errors and the absence thereof}
@@ -144,7 +145,7 @@ invalid pointer accesses,\ldots
\listinginputcaption{1}{\texttt{rte.c}}{rte.c}
When launched with \lstinline|frama-c -val rte.c|,
-the value analysis emits a warning about an out-of-bound access at line 5:
+EVA emits a warning about an out-of-bound access at line 5:
\begin{logs}
rte.c:5:[kernel] warning: accessing out of bounds index. assert i < 10;
\end{logs}
@@ -152,37 +153,45 @@ There is in fact an out-of-bounds access at this line in the program.
It can also happen that, because of approximations during its computations,
Frama-C emits warnings for constructs
that do not cause any run-time errors. These are called ``false alarms''.
-On the other hand, the fact that the value analysis
+On the other hand, the fact that EVA
computes correct, over-approximated sets of possible values prevents it
from remaining silent on a program that contains a run-time error. For
instance, a particular division in the analyzed program
is the object of a warning
as soon as the set of possible values for the divisor
contains zero. Only
-if the set of possible values computed by the
-value analysis does not contain zero is the warning omitted, and
+if the set of possible values computed by EVA
+does not contain zero is the warning omitted, and
that means that the divisor really cannot be null at run-time.
-\section{Other analyses based on the value analysis}
+\section{From Value Analysis to EVA}
+
+The EVA plug-in was previously called the \emph{Value Analysis plug-in}.
+Following major changes in its expressivity and overall precision,
+the plugin was subsequently renamed to \emph{Evolved Value Analysis}, or
+EVA for short. Those changes were first made available with the
+Aluminium version of Frama-C. They are presented in section~\ref{sec:eva}.
+
+\section{Other analyses based on EVA}
Frama-C also provides
synthetic information on the behavior of analyzed functions:
inputs, outputs, and dependencies. This information is computed
-from the results of the value analysis plug-in,
-and therefore some familiarity with the value analysis
+from the results of the EVA plug-in,
+and therefore some familiarity with EVA
is necessary to get the most of these computations.
\chapter{Tutorial}\label{tutorial}
\vspace{2cm}
-{\em Some use cases for the value analysis\ldots}
+{\em Some use cases for EVA\ldots}
\vspace{2cm}
\section{Introduction}
Throughout this tutorial, we will see on a single example how to use
-the value analysis for the following tasks :
+EVA for the following tasks :
\begin{enumerate}
\item to get familiar with foreign code,
\item to produce documentation automatically,
@@ -255,28 +264,27 @@ of the function. Using static analysis for verifying that a piece
of code corresponds to the mathematical model
which was the object of the security proofs is an interesting
topic but is outside the scope of this tutorial.
-In this document, we will not be using the value analysis for
+In this document, we will not be using EVA for
verifying cryptographic properties.
-We will, however, use the value analysis to familiarize ourselves
+We will, however, use EVA to familiarize ourselves
with Skein's reference implementation, and we will see that
-Frama-C's value analysis can be a more useful tool than, say, a C
-compiler, to this effect. We will also use the value analysis to look
+it can be a more useful tool than, say, a C
+compiler, to this effect. We will also use EVA to look
for bugs in the implementation of Skein, and finally prove that the
functions that implement Skein may never cause a run-time error for a
general use pattern. Because of the numerous pitfalls of the C
programming language, any amount of work at the
mathematical level cannot exclude the possibility of problems
such as buffer overflows in the implementation.
-It is a good thing to be able to rule these out with Frama-C's
-value analysis.
+It is a good thing to be able to rule these out with EVA.
-Frama-C's value analysis is most useful for embedded or embedded-like
+EVA is most useful for embedded or embedded-like
code. Although the Skein library does not exactly fall in this category,
it does not demand dynamic allocation and uses few functions from external
libraries, so it is well suited to this analysis.
-\section{Using the value analysis for getting familiar with Skein}
+\section{Using EVA for getting familiar with Skein}
\subsection{Writing a test}
@@ -351,10 +359,10 @@ gcc *.c
13
\end{logs}
-\subsection{First try at a value analysis}
+\subsection{First try at an analysis using EVA}
-Let us now see how Frama-C's value analysis works on the same example.
-The value analysis can be launched with the following command.
+Let us now see how EVA works on the same example.
+EVA can be launched with the following command.
The analysis should not take more than a few seconds:
\begin{listing-nonumber}
frama-c -val *.c >log
@@ -369,7 +377,7 @@ would be during an actual compilation.
There are analyses where the influence of host platform parameters
is not noticeable. The analysis we are embarking on is not one of them.
If you pre-process the Skein source code with a 64-bit compiler and
-then analyze it with Frama-C targetting its default 32-bit platform,
+then analyze it with Frama-C targeting its default 32-bit platform,
the analysis will be meaningless and you won't be able to make sense of
this tutorial.
If you are using a 64-bit compiler, simply match
@@ -379,7 +387,7 @@ this tutorial.
The ``\lstinline|>log|'' part of the command sends all
the messages emitted by Frama-C into a file named
-``\lstinline|log|''. The value analysis is verbose for a number of reasons that
+``\lstinline|log|''. EVA is verbose for a number of reasons that
will become clearer later in this tutorial.
The best way to make sense of the information
produced by the analysis is
@@ -411,7 +419,7 @@ lines of the log.
Since we are trying out the library for the first time,
something else to look for in the log file is the list of functions for
-which the source code is missing. The value analysis requires
+which the source code is missing. EVA requires
either a body or a specification for each function it analyses.
\begin{listing-nonumber}
@@ -426,7 +434,7 @@ already has prototypes for the most important library functions.
But suppose you would have a custom printing
function, say \verb|print| instead of \verb|printf|, or some other function
with missing source code. For instance, change the code in \verb|main_1.c|,
-replacing \verb|printf| with \verb|print|, re-run the value analysis,
+replacing \verb|printf| with \verb|print|, re-run EVA,
and then grep the log again. You will obtain this output:
\begin{logs}
@@ -434,10 +442,10 @@ main_1.c:14:[kernel] warning: Neither code nor specification for function print,
generating default assigns from the prototype
\end{logs}
-The warning indicates that the value analysis is trying to infer an
+The warning indicates that EVA is trying to infer an
{\em assigns} clause for the function. This will be explained in detail later
-(\ref{annot_assigns}), but for now the important part is that the value
-analysis needs either source code or an ACSL specification in order to work.
+(\ref{annot_assigns}), but for now the important part is that EVA
+needs either source code or an ACSL specification in order to work.
Without those, it can only guess what each function does from the function's
prototype, which is both inaccurate and likely incorrect.
@@ -462,9 +470,9 @@ frama-c -metrics -metrics-libc *.c
This command computes, among other pieces of information,
a list of missing functions using
a syntactic analysis. It is not exactly equivalent to
-grepping the log of the value analysis because it lists
+grepping the log of EVA because it lists
all the functions that are missing, while the log of
-the value analysis only cites the functions that would have
+EVA only cites the functions that would have
been necessary to an analysis. When
analyzing a small part of a large codebase, the latter list
may be much shorter than the former.
@@ -509,7 +517,7 @@ name ``\lstinline|lib.c|''.
%% under the name ``\lstinline|string.h|''
%% \listinginput{1}{tutorial/string.h}
-%% In some circumstances, the results of the value analysis may
+%% In some circumstances, the results of EVA may
%% remain useful even when letting Frama-C guess the effects
%% of missing functions. In the case of functions that take
%% pointers as arguments, however, the possibilities are too numerous
@@ -520,7 +528,7 @@ name ``\lstinline|lib.c|''.
%% it does not have effects on the variables of the program.
%. It is generally far simpler to provide
-%either the actual code or a modelization written in C
+%either the actual code or a model written in C
%for the missing functions.
\subsection{First meaningful analysis}
@@ -547,7 +555,7 @@ alongside the transformed one.
A quick inspection shows that the Skein functions
use variable \lstinline|ONE| to detect endianness.
Frama-C assumes a little-endian architecture
-by default, so the value analysis is only analyzing the
+by default, so EVA is only analyzing the
little-endian version of the library (Frama-C
also assumes an IA-32 architecture, so we are only
analyzing the library as compiled and run on this architecture).
@@ -561,7 +569,7 @@ These are all variables coming from ACSL specifications in the Frama-C
standard library.
Next in the log are a lot of entries that simply indicate
-the value analysis' progression. When the analysis
+EVA's progression. When the analysis
takes too long, these messages
help the user understand where time is spent.
We can ignore these messages now. The following line
@@ -598,9 +606,9 @@ has to be a valid pointer.
\end{listing-nonumber}
The command \lstinline|frama-c *.c -val -print| launches
-the value analysis and then prints the transformed source code,
+EVA and then prints the transformed source code,
annotated with the
-alarms raised by the value analysis. In our case, the
+alarms raised by EVA. In our case, the
function \lstinline|memset| is transformed in
\begin{listing-nonumber}
void *memset(void *dest, int val, size_t len)
@@ -629,7 +637,7 @@ void *memset(void *dest, int val, size_t len)
As we will find out later in this tutorial, this alarm is a false
alarm, an indication of a potential problem in a place where there is
-in fact none. On the other hand, the value analysis never remains
+in fact none. On the other hand, EVA never remains
silent when a risk of run-time error is present, unlike many other
static analysis tools. The important consequence is that if you get
the tool to remain silent, you have {\em formally verified} that
@@ -711,14 +719,14 @@ You can also use the Back button (left arrow) in the toolbar.
Because we compiled and executed the same program that we are
now analyzing, we are confident that most of the alarms
-displayed by the value analysis are false alarms that do not
+displayed by EVA are false alarms that do not
correspond to actual problems. In fact, because the program
is deterministic and takes no inputs,
only one of the alarms can be a true alarm in
the strictest sense. The analysis stops when an error is
encountered (what would it even mean to continue the analysis
after, for instance, \lstinline|NULL| has been dereferenced?).
-It is only because the value analysis is uncertain about the errors
+It is only because EVA is uncertain about the errors
encountered here that it continues and finds more possible
errors.
@@ -737,7 +745,7 @@ and \lstinline|else| branches of a conditional statement.
This makes the analysis more precise (at the cost of being
slower) for almost every program that can be analyzed.
-The value analysis has different ways to provide information on
+EVA has different ways to provide information on
the loss of precision that causes the false alarms.
This is another reason why it is so verbose during an analysis:
it tries to provide enough information for a motivated user
@@ -748,7 +756,7 @@ and what instructions in the program made them imprecise.
But instead of spending precious human time making use
of the provided information, the brute-force approach of blindly
applying the \lstinline|-slevel| option must be tried first.
-Indeed, \lstinline|-slevel| is one of the value analysis options
+Indeed, \lstinline|-slevel| is one of the options of EVA
that can never cause it to become incorrect. Such options,
when used wrongly, may make the analysis slower,
provide hints that are not
@@ -827,7 +835,7 @@ finds that function \lstinline|main| does not terminate.
The next warning, \lstinline|accessing uninitialized left-value...|
is emitted whenever an accessed value may be uninitialized, and the emitted
assertion, \lstinline|\initialized(&hash[i])|, could not be verified by
-the value analysis, and must therefore be verified by other means
+EVA, and must therefore be verified by other means
(eventually, other Frama-C analyses) to ensure the behavior of the code is
defined.
@@ -837,7 +845,7 @@ There were three alarms in the analysis. The other two are related to
interactions between
the Frama-C standard library and our own implementations of \verb|memset|/
\verb|memcpy|\footnote{Namely, the fact that their specifications involve
-{\em logic predicates} that are not yet understood by the value analysis leads
+{\em logic predicates} that are not yet understood by EVA leads
to an ``Unknown'' status, even though they are valid in this case.},
but we can safely ignore them here.
@@ -858,7 +866,7 @@ but we can safely ignore them here.
%% \lstinline|printf| is a constant value, independent of its arguments),
%% but since we ignore its result in our code anyway, this is fine here.
%% This is by the way equivalent to the default behavior that was previously
-%% inferred by the value analysis, and the reason why it emitted warnings:
+%% inferred by EVA, and the reason why it emitted warnings:
%% it is not a correct specification in the general case.
Furthermore, the program
@@ -943,7 +951,7 @@ that we wish to study:
From this point onward the program is no longer executable because
of the call to builtin primitives such as \lstinline|Frama_C_interval|.
We therefore dispense with the final calls to \lstinline|printf|,
-since the value analysis offers simpler ways to observe intermediate
+since EVA offers simpler ways to observe intermediate
and final results. Note that we included \verb|__fc_builtin.h|, a file
that comes from the Frama-C distribution and which
defines \lstinline|Frama_C_interval|. Running Frama-C on this
@@ -970,7 +978,7 @@ that is passed to \lstinline|Skein_256_Final| (all 8 bytes of the buffer),
to compute the new contents of this buffer from the contents of the
input buffer \lstinline|msg| (all 80 bytes of it), and from nothing else.
-During the value analysis, we have seen that all of the buffer \verb|hash|
+During EVA's analysis, we have seen that all of the buffer \verb|hash|
was always modified in the conditions of the analysis: the reason is that
this buffer was uninitialized before the sequence of calls,
and guaranteed to be initialized after them.
@@ -978,7 +986,7 @@ and guaranteed to be initialized after them.
We can get the complete list of locations that may be modified by each
function by adding the option \verb|-out| to the other options we were
already using. These locations are computed in a quick analysis that comes
-after the value analysis. In the results of this analysis, we find:
+after EVA. In the results of this analysis, we find:
\begin{logs}
[inout] Out (internal) for function main:
Frama_C_entropy_source; msg[0..79]; i; hash[0..7]; skein_context; tmp
@@ -1024,7 +1032,7 @@ locations that exclude each function's local variables, we get:
This means that no location other than \lstinline|hash[0..7]| was
modified by the sequence of calls to Skein-256 functions. It doesn't
mean that each of the cells of the array was overwritten: we have to
-rely on the results of the value analysis when \lstinline|hash| was a
+rely on the results of EVA when \lstinline|hash| was a
local variable for that result. But it means that when used in
conformance with the pattern in this program, the functions do not
accidentally modify a global variable. We can conclude from this
@@ -1032,7 +1040,7 @@ analysis that the functions are re-entrant as long as the concurrent
computations are being made with separate contexts and destination
buffers.
-Keeping the convenient function \lstinline|do_Skein_256| for modelizing the
+Keeping the convenient function \lstinline|do_Skein_256| for modeling the
sequence, let us now compute the functional dependencies of each function.
Functional dependencies list, for each output location,
the input locations that influence the final contents of this output location:
@@ -1086,7 +1094,7 @@ guaranteed to be over-written with a value that depends only on
various other subfields of \lstinline|skein_context.h|. On the other
hand, the \verb|-deps| analysis does not guarantee that all cells of
\verb|hash| are over-written --- but we previously saw we
-could deduce this information from the value analysis' results.
+could deduce this information from EVA's results.
Since we don't know how the functions are supposed to work,
it is difficult to tell if these
@@ -1126,7 +1134,7 @@ A stronger property to verify would be that the
sequence \lstinline|Init(...)|, \lstinline|Update(...,80)|,
\lstinline|Final(...)| computes the same hash as when the
same message is passed in two calls \lstinline|Update(...,40)|.
-This property is beyond the reach of the value analysis.
+This property is beyond the reach of EVA.
In the advanced tutorial, we show how to verify easier properties
for sequences of calls that include several calls
to \lstinline|Update|.
@@ -1140,7 +1148,7 @@ between \lstinline|Init| and \lstinline|Final|. The general strategy
is to modify the C analysis context we have already written in a way
such that it is evident that it captures all such sequences of calls,
and also in a way that launched with adequate options,
-the value analysis does not emit any warning.
+EVA does not emit any warning.
The latter condition is harder than the former.
Observing results (with the GUI or observation functions
@@ -1158,7 +1166,7 @@ available posts in chronological order.
% One of the strong properties that we will verify is that
% it is {\em platform-conforming}\footnote{The notion here is almost the same as
% that of {\em strictly conforming program} in the ``Conformance'' chapter of the
-% C99 standard, but the value analysis recognizes some widely-used constructs
+% C99 standard, but EVA recognizes some widely-used constructs
% that are not specified in the standard, as discussed in \ref{norme_pratique}}: for
% a given platform configuration,
% two sequences of calls to the Skein-256 functions, part of the same
@@ -1182,7 +1190,7 @@ available posts in chronological order.
-\chapter{What the value analysis provides}\label{what}
+\chapter{What EVA provides}\label{what}
\vspace{2cm}
%\begin{figure}[h]
@@ -1192,13 +1200,13 @@ available posts in chronological order.
%\newpage
{\em Here begins the reference section of this manual.\\
-This chapter categorizes and describes the outputs of the value analysis.}
+This chapter categorizes and describes the outputs of EVA.}
\vspace{2cm}
\section{Values}
-The value analysis plug-in accepts queries for the value of
+The EVA plug-in accepts queries for the value of
a variable \lstinline|x| at a given program point. It answers such a
query with an over-approximation of the set of values possibly taken
by \lstinline|x| at the designated point for all possible executions.
@@ -1255,7 +1263,7 @@ Each $a_i$ is of the form:
may be used, i.e. \verb+&t{[1].i1, [2].i2}+.
\item $\mbox{\tt NULL} + D$, which denotes absolute addresses (seen
as offsets with respect to the base address NULL).
- \item $\mbox{\tt "foo"} + D$, which denotes offsets from a litteral
+ \item $\mbox{\tt "foo"} + D$, which denotes offsets from a literal
string with contents ``foo''.
\end{itemize}
In all three cases, ``${}+D$'' is omitted if $D$ is $\{0\}$, that is,
@@ -1291,15 +1299,14 @@ values that were found at the memory location.
Most modern C compilation platforms unify integer values
and absolute addresses:
there is no difference between the encoding of the integer 256
-and that of the address \lstinline|(char*)0x00000100|. Therefore, the
-value analysis
+and that of the address \lstinline|(char*)0x00000100|. Therefore, EVA
does not distinguish between these two values either. It is partly
for this reason that offsets $D$ are expressed
in bytes in domains of the form $\cbopen\cbopen \&x + D;\ \ldots\ \cbclose\cbclose$.
-In floating-point computations, the value analysis considers that
+In floating-point computations, EVA considers that
obtaining NaN, $+\infty$, or $-\infty$
is an unwanted error. The floating-point intervals provided by
the analysis are always intervals of finite floating-point values.
@@ -1432,12 +1439,12 @@ In this example, the return value for \lstinline|f| is\\
\lstinline|{{ garbled mix of &{ x; y } (origin: Arithmetic { ari.c:4 }) }}|.
-\section{What is checked by the value analysis}\label{obligations}
+\section{What is checked by EVA}\label{obligations}
-The value analysis warns about possible run-time errors in the analyzed
+EVA warns about possible run-time errors in the analyzed
program, through the means of \emph{proof obligations}: the errors that cannot
-be proved by the value analysis plugin are left to be proved by other plugins.
-%% The correctness of the results provided by the value analysis
+be proved by the EVA plug-in are left to be proved by other plug-ins.
+%% The correctness of the results provided by EVA
%% is guaranteed only if the user verifies all the
%% proof obligations generated during the analysis.
These proof obligations
@@ -1454,7 +1461,7 @@ annotated with the proofs obligations. The companion option
annotated source code to be written to.
\subsubsection{Invalid memory accesses}
-Whenever the value analysis is not able to establish that
+Whenever EVA is not able to establish that
a dereferenced pointer is valid, it emits an alarm that expresses
that the pointer needs to be valid at that point. Likewise, direct
array accesses that may be invalid are flagged.
@@ -1477,7 +1484,7 @@ page \pageref{unsafe-arrays}.
Note that line 6 or 8 in this example could be considered as
problematic in the strictest interpretation of the standard.
-The value analysis omits warnings for these two lines according
+EVA omits warnings for these two lines according
to the attitude described in \ref{norme_pratique}. An option
to warn about these lines could happen if there was demand for
this feature.
@@ -1527,19 +1534,19 @@ shift.c:4: ... invalid RHS operand for shift. assert 0 <= c < 32;
\end{logs}
The ISO C99 standard also forbids left-shifting a negative
-integer. This is also detected by the value analysis.
+integer. This is also detected by EVA.
-\listinginput{1}{shift.c}
+\listinginput{1}{lshift.c}
\begin{logs}
lshift.c:4:[kernel] warning: invalid LHS operand for left shift. assert 0 <= x;
\end{logs}
\subsubsection{Overflow in integer arithmetic}
-By default, the value analysis emits alarms for --- and reduces the
+By default, EVA emits alarms for --- and reduces the
sets of possible results of --- signed arithmetic computations where
the possibility of an overflow exists. Indeed,
-such overflows have an undefined behavior acccording to
+such overflows have an undefined behavior according to
paragraph 6.5.5 of the ISO/IEC 9899:1999 standard.
%
If useful, it is also possible to assume that signed integers overflow
@@ -1564,8 +1571,8 @@ integers. In the signed case, the least significant bits
of the original value are used, and are interpreted according
to 2's complement representation.
Frama-C's options \lstinline|-warn-signed-downcast| and
-\lstinline|-warn-unsigned-downcast| are not honored by the value analysis.
-The RTE plugin can be used to generate the relevant assertions
+\lstinline|-warn-unsigned-downcast| are not honored by EVA.
+The RTE plug-in can be used to generate the relevant assertions
before starting an analysis.
@@ -1628,7 +1635,7 @@ if it appears to manipulate the address of a local variable outside
of the scope of said variable. Both issues occur in the following
example:
\listinginput{1}{uninitialized.c}
-The value analysis emits alarms for lines 5
+EVA emits alarms for lines 5
(variable \lstinline|r| may be uninitialized)
and 13 (a dangling pointer to local variable \lstinline|t| is used).
\begin{logs}
@@ -1637,9 +1644,9 @@ uninitialized.c:13: ... accessing left-value that contains escaping addresses.
assert !\dangling(&p);
\end{logs}
-By default, the value analysis does not emit an alarm for a copy from memory
+By default, EVA does not emit an alarm for a copy from memory
to memory when the copied values include dangling addresses or uninitialized
-contents. This behavior is safe because the value analysis warns later, as soon
+contents. This behavior is safe because EVA warns later, as soon
as an unsafe value is used in a computation --either directly or
after having been copied from another location.
The copy operations for which alarms are not emitted are assignments
@@ -1674,20 +1681,20 @@ behavior of the compiler is in general undesirable (although
this one is rather benign for current compilation platforms).
Although these alarms may seem unimportant, they should still be
-checked, because the value analysis may reduce the propagated states
+checked, because EVA may reduce the propagated states
accordingly to the emitted alarm. For instance, for the
\lstinline|&x+2 != NULL| comparison, after emitting the alarm that the
quantity \lstinline|&x+2| must be reliably comparable to 0, the
analysis assumes that the result of the comparison is 1. The
consequences are visible when analyzing the following example:
\listinginput{1}{pointer_comparison.c}
-The value analysis finds that this program does not terminate.
+EVA finds that this program does not terminate.
This seems incorrect because an actual execution will terminate
on most architectures.
-However, the value analysis' conclusion is conditioned by
+However, EVA's conclusion is conditioned by
an alarm emitted for the pointer comparison.
-The value analysis only allows pointer comparisons that give
+EVA only allows pointer comparisons that give
reproducible results --- that is, the possibility of obtaining an
unspecified result for a pointer comparison is considered as an
unwanted error, and is excluded by the emission of an alarm.
@@ -1698,7 +1705,7 @@ option \lstinline|-undefined-pointer-comparison-propagate-all|.
With this option, in the example program above,
the values \lstinline|0| and \lstinline|1| are considered as results
for the condition as soon as \lstinline|p| becomes an invalid address.
-Therefore, the value analysis does not predict that the program
+Therefore, EVA does not predict that the program
does not terminate.
Conversely, verifications for undefined pointer comparisons can be
@@ -1745,7 +1752,7 @@ se.c:5:[kernel] warning: Unspecified sequence with side effect:
y = x + tmp;
\end{logs}
-Then the value analysis is run on the program.
+Then EVA is run on the program.
In the example at hand, the analysis finds problems at lines 5 and 7.
\begin{logs}
se.c:5: ... undefined multiple accesses in expression. assert \separated(&x, &x);
@@ -1766,7 +1773,7 @@ is \lstinline|y = f() + g();|. For this statement, it is
unspecified which function will be called first. If one of them
modifies global variables that are read by the other, different
results can be obtained depending on factors outside the programmer's
-control. At this time, the value analysis does not check if these
+control. At this time, EVA does not check if these
circumstances occur, and silently chooses an order for calling
\lstinline|f| and \lstinline|g|. The statement
\lstinline|y = f() + x++;|
@@ -1777,7 +1784,7 @@ These limitations will be addressed in a future version.
\subsubsection{Partially overlapping lvalue assignment}
Vaguely related to, but different from, undefined side-effects in expressions,
-the value analysis warns about the following program:
+EVA warns about the following program:
\listinginput{1}{overlap.c}
@@ -1791,7 +1798,7 @@ and it returns 0 when compiled with \lstinline|gcc -m32|.
For a
program as simple as the above, all these compilers are
supposed to implement the same implementation-defined choices. Which
-compiler, if we may ask such a rethorical
+compiler, if we may ask such a rhetorical
question, is right? They all are, because the program is undefined.
When function \lstinline|copy()| is called from \lstinline|main()|,
the assignment \lstinline|*p = *q;| breaks
@@ -1802,12 +1809,12 @@ the left and right lvalues must overlap either exactly or not at all.
The program breaking this rule means compilers neither have to emit
warnings (none of the above did) nor produce code that does what the
programmer intended, whatever that was.
-Launched on the above program, the value analysis says:
+Launched on the above program, EVA says:
\begin{logs}
partially overlapping lvalue assignment. assert p == q || \separated(p, q);
\end{logs}
-By choice, the value analysis does not emit alarms for overlapping
+By choice, EVA does not emit alarms for overlapping
assignments of size less than \lstinline|int|, for which reading and
writing are deemed atomic operations. Finding the exact cut-off point
for these warnings would require choosing a specific compiler and
@@ -1817,12 +1824,12 @@ for a specific target platform and compiler.
\subsubsection{Invalid function pointer access}
-When the value analysis encounters a statement of the form \lstinline|(*e)(x);|
+When EVA encounters a statement of the form \lstinline|(*e)(x);|
and is unable to guarantee that expression \lstinline|e|
evaluates to a valid function address, an alarm is emitted. This includes
invalid pointers (such as \lstinline|NULL|), or pointers to a function
with an incompatible type. In the latter case, an alarm is emitted,
-but the value analysis may nevertheless proceed with the analysis
+but EVA may nevertheless proceed with the analysis
if it can give some meaning to the call. This is meant to account
for frequent misconceptions on type compatibility (e.g. \lstinline|void *|
and \lstinline|int *| are \emph{not} compatible).
@@ -1844,10 +1851,10 @@ valid_function.c:12:[value] assertion 'Value,function_pointer' got final status
%TODO: alarm for pointer subtraction
-\section{Log messages emitted by the value analysis}
+\section{Log messages emitted by EVA}
-This section categorizes the non-alarms related messages displayed by the
-value analysis in \lstinline|frama-c|, the batch version of the analyzer.
+This section categorizes the non-alarms related messages displayed by EVA
+in \lstinline|frama-c|, the batch version of the analyzer.
When using \lstinline|frama-c-gui| (the graphical interface), the messages
are directed to different panels in the bottom right of the main window
for easier access.
@@ -1869,7 +1876,7 @@ hold whenever the end of this function is reached.
% snowball
Some messages warn that the analysis is making an operation likely
to cause loss of precision. Other messages warn the user that
-unusual circumstances have been encountered by the value analysis.
+unusual circumstances have been encountered by EVA.
In both these cases, the messages are not proof
obligations and it is not mandatory for the user to act on them.
@@ -1880,7 +1887,7 @@ are intended to help the user trace the results of the analysis, and
give as much information as possible in order to help
em find when and why the analysis becomes imprecise.
These messages are only useful when it is important to analyze the application
-with precision. The value analysis remains correct even when it
+with precision. EVA remains correct even when it
is imprecise.
\smallskip
@@ -1926,7 +1933,7 @@ find where the analyzer spends its time.
When writing a Frama-C plug-in to assist in
reverse-engineering source code, it does not really make sense to expect
-the user to check the alarms that are emitted by the value analysis.
+the user to check the alarms that are emitted by EVA.
Consider for instance Frama-C's slicing plug-in. This plug-in produces
a simplified version of a program. It is often applied to large unfamiliar
codebases; if the user is at the point where ey needs a slicer to make
@@ -1952,10 +1959,10 @@ exits abruptly on most architectures, whereas the sliced version
computes the value of \lstinline|x|.
It is fine to ignore alarms in this context,
-but the user of a code comprehension plug-in based on the value analysis
+but the user of a code comprehension plug-in based on EVA
should study the categorization of alarms in section \ref{obligations}
with particular care.
-Because the value analysis is more aggressive
+Because EVA is more aggressive
in trying to extract precise information from the program than other
analyzers, the user is more likely to observe incorrect results if there
is a misunderstanding between him and the tool about what assumptions
@@ -1967,21 +1974,20 @@ assuming that a signed overflow wraps around in 2's complement
representation? Function \lstinline|memmove|, for instance, typically does the
former when applied to two addresses with different bases.
%
-Yet, currently, if there appears to be an undefined pointer comparison, the
-value analysis propagates a state that may contain only ``optimistic''
+Yet, currently, if there appears to be an undefined pointer comparison, EVA
+propagates a state that may contain only ``optimistic''
(assuming the undefined circumstances do not occur) results
for the comparison result and for the pointers.\footnote{As explained earlier, in this particular case, it is
possible to get all possible behaviors using option
\lstinline|-undefined-pointer-comparison-propagate-all|.}
-It is possible to take advantage of the value analysis
+It is possible to take advantage of EVA
for program comprehension, and all existing program comprehension
tools need to make assumptions about undefined behaviors. Most tools
do not tell whether they had to make assumptions or not.
-The value analysis
-does: each alarm, in general,
+EVA does: each alarm, in general,
is also an assumption. Still, as implementation progresses
-and the value analysis
+and EVA
becomes able to extract more information from the alarms it emits,
one or several options
to configure it either not to emit some alarms, or not
@@ -2002,17 +2008,17 @@ The variation domain thus obtained
contains all the values that this lvalue or expression may
have anytime an actual execution reaches the selected statement.
-In fact, from the point view of the value analysis, the graphical interface
+In fact, from the point view of EVA, the graphical interface
that allows to observe the values of variables in the program is very much
an ordinary Frama-C plug-in. It uses the same functions (registered
in module \lstinline|Db.Value|) as other plug-ins that interface with
-the value analysis.
+EVA.
This API is not very well documented yet, but one early external
-plug-in author used the GUI to get a feeling of what the value analysis
+plug-in author used the GUI to get a feeling of what EVA
could provide, and then used the OCaml source code of the GUI as
a reference for obtaining this information programmatically.
-\subsection{Value analysis API overview}
+\subsection{EVA API overview}
The function \lstinline|!Db.Value.access| is one of the
functions provided to custom plug-ins.
@@ -2053,22 +2059,22 @@ developing a custom plug-in.
\vspace{2cm}
This chapter describes how the difficult constructs in the C language
-are handled in the value analysis. The constructs listed
+are handled in EVA. The constructs listed
here are difficult for all static analyzers in general.
Different static analysis techniques can often be positioned
with respect to each other by looking only at how they handle loops,
function calls and partial codebases.
-The value analysis works best on embedded code
+EVA works best on embedded code
or embedded-like code without multithreading,
-although it is usable (with modelization work from the user) on
+although it is usable (with modeling work from the user) on
applications that include it. Dynamic allocation is supported in
limited form, but imprecisions may accumulate quickly
(e.g. linked lists often lead to suboptimal results).
\section{Prospective features}
-The value analysis does not check all the properties that could be
+EVA does not check all the properties that could be
expected of it\footnote{There are 245 unspecified or undefined
behaviors in Annex J of the ISO C99 standard.}. Support for each of
these missing features could arrive if the need was expressed. Below
@@ -2076,7 +2082,7 @@ are some of the existing limitations.
\subsection{Strict aliasing rules}
-The value analysis does not check that the analyzed program uses
+EVA does not check that the analyzed program uses
pointer casts in a way that is compatible with strict aliasing
rules. This is one of the major current issues of the C world because
compilers only recently began to take advantage of these rules for
@@ -2091,12 +2097,12 @@ of such a memory location is a constant string literal
(\lstinline|"foo"|). The ACSL specification language sports a
predicate \lstinline|\valid_read| to express that a memory location is
valid for reading but does not have to be valid for writing.
-Accordingly, the value analysis emits alarms using
+Accordingly, EVA emits alarms using
\lstinline|\valid_read(lv)| when an lvalue \lstinline|lv| is read from, and
\lstinline|\valid(lv)| when \lstinline|lv| is written to.
Variables with a const-qualified type are among the memory locations
-that the value analysis knows to be good to read from but forbidden to
+that EVA knows to be good to read from but forbidden to
write to. However, the \lstinline|const| type qualifier is currently only
handled when placed at the top-level of the type of a global variable
or formal argument. Other \lstinline|const| locations are considered
@@ -2104,7 +2110,7 @@ writable.
\subsection{Alignment of memory accesses}
-The value analysis currently does not check that memory accesses are
+EVA currently does not check that memory accesses are
properly aligned in memory. It assumes that non-aligned accesses have
only a small time penalty (instead of causing an exception) and that the
programmer is aware of this penalty and is accessing (or seems to be accessing)
@@ -2124,7 +2130,7 @@ The analysis of a source program always takes a finite time.
The fact that the source code contains loops, and that some of these
loops do not terminate, can never induce the analyzer itself to loop forever.
% \footnote{An exception to this rule is when one uses the most
-% precise modelizations of {\tt malloc} (details in section
+% precise modeling of {\tt malloc} (details in section
% \ref{malloc}).}
In order to guarantee this property, the analyzer may need to
introduce approximations when analyzing a loop.
@@ -2134,7 +2140,7 @@ Let us assume, in the following lines, that the function \lstinline|c|
is unknown:
\listinginput{1}{boucles.c}
-The value analysis plug-in could provide the best possible sets of values
+The EVA plug-in could provide the best possible sets of values
if the user explicitly instructed it to study step by step each
of the hundred loop iterations. Without any such instruction,
it analyses the body of the loop much less than
@@ -2164,11 +2170,11 @@ than \lstinline|printf|, and the observation primitives of Frama-C
GUI more than make up for the absence of \lstinline|printf|.
Recursive functions are allowed in Frama-C, but they
-are not handled in the current version of the value analysis plug-in.
+are not handled in the current version of the EVA plug-in.
\section{Analyzing a partial or a complete application}
-The default behavior of the value analysis plug-in allows to
+The default behavior of the EVA plug-in allows to
analyze complete applications,
that is, applications for which the source code is entirely
available. In practice, it is sometimes desirable to limit the analysis
@@ -2204,7 +2210,7 @@ The entry point of the analyzed application can be specified
on the command line using the option \lstinline|-main| (section \ref{entry}).
In the GUI,
it is also possible to specify the name of the entry point at
-the time of launching the value analysis.
+the time of launching EVA.
\subsection{Entry point of an incomplete application}
@@ -2237,7 +2243,7 @@ analyzer.
\subsection{Choosing between complete and partial application mode}
This section uses a small example to illustrate the pitfalls that should
-be considered when using the value analysis with an incomplete
+be considered when using EVA with an incomplete
part of an application.
This example is simplified but quite typical. This is the pattern followed
by the complete application:
@@ -2265,7 +2271,7 @@ void main(void) {
If \lstinline|init2| is analyzed as the entry point of a complete application,
or if the function \lstinline|init1| is accidentally omitted, then
-at the time of analyzing \lstinline|init2|, the value analysis will have no reason
+at the time of analyzing \lstinline|init2|, EVA will have no reason
to believe that the global variable \lstinline|ok1| has not kept its initial value 0.
The analysis of \lstinline|init2| consists of determining
that the value of the \lstinline|if| condition is always false, and to ignore
@@ -2280,7 +2286,7 @@ It is also possible to use annotations to describe the state in which
the analysis should be started as a precondition for the entry point
function. The syntax and usage of preconditions is described in
section \ref{prepostasserts}. The user should pay attention to the
-intrinsic limitations in the way the value analysis interprets these
+intrinsic limitations in the way EVA interprets these
properties (section \ref{reduction_proprietes}). A simpler alternative
for specifying an initial state is to build it
using the non-deterministic
@@ -2297,13 +2303,13 @@ or break it down into elementary sub-pieces, the same way unit tests do.
\subsection{Applications relying on software interrupts}
-The current version of the value analysis plug-in is not able to
+The current version of the EVA plug-in is not able to
take into account
interrupts (auxiliary function that can be executed at any time
during the main computation). As things stand, the plug-in may give
answers that do not reflect reality if interrupts play a role
in the behavior of the analyzed application.
-There is preliminary support for using the value analysis in this
+There is preliminary support for using EVA in this
context in the form of support for \lstinline|volatile| variables.
Unlike normal variables, the analyzer does not assume that
@@ -2325,7 +2331,7 @@ also have non-volatile access paths to them.
\section{Conventions not specified by the ISO standard}
-The value analysis can provide useful information even for low-level
+EVA can provide useful information even for low-level
programs that rely on non-portable C construct and that depend
on the size of the word and the endianness of the target architecture.
@@ -2334,8 +2340,8 @@ on the size of the word and the endianness of the target architecture.
There exists constructs of the C language which the ISO standard does
not specify, but which are compiled in the same way by almost every compiler
-for almost every architecture. For some of these constructs, the
-value analysis plug-in assumes a reasonable compiler and
+for almost every architecture. For some of these constructs, the EVA
+plug-in assumes a reasonable compiler and
target architecture. This design choice makes it possible to obtain more
information about the behavior of the program than would be possible
using only what is strictly guaranteed by the standard.
@@ -2365,8 +2371,8 @@ programmer did not know exactly how the non-portable version will be
translated by eir compiler. But the portable version may
produce a code which is significantly slower and/or bigger. In practice,
the constraints imposed on embedded software often lead to choosing
-the non-portable version. This is why, as often as possible, the value
-analysis uses the same standard as the one used by programmers,
+the non-portable version. This is why, as often as possible, EVA
+uses the same standard as the one used by programmers,
the unwritten one.
It is the experience gained on actual industrial software, during
the development of early versions of Frama-C as well as during
@@ -2376,8 +2382,8 @@ the development of other tools, that led to this choice.
The hypotheses discussed here have to do with the conversions
between integers and pointers, pointer arithmetic, the representation
of \lstinline|enum| types and the relations between the addresses of the
-fields of a same \lstinline|struct|. As a concrete example, the value
-analysis plug-in assumes two-complement representation,
+fields of a same \lstinline|struct|. As a concrete example, EVA
+plug-in assumes two-complement representation,
which the standard does not guarantee,
and whose consequences can be seen when converting between
signed and unsigned types or with signed arithmetic overflows.
@@ -2393,12 +2399,12 @@ to a fixed ABI that ensures the reproducibility of compilation choices.
\section{Memory model -- Bases separation}\label{bases}
This section introduces the abstract representation of the memory
-the value analysis relies on. It is necessary to have
+EVA relies on. It is necessary to have
at least a superficial idea of this representation in order to
interact with the plug-in.
\subsection{Base address}
-The memory model used by the value analysis relies on the classical notion
+The memory model used by EVA relies on the classical notion
of ``base address''. Each variable, be it local or global, defines one
and only one base address.
\goodbreak
@@ -2464,8 +2470,7 @@ respect this hypothesis, the user should simply verify the generated
proof obligations to ensure the correctness of the analysis.
For the programs that voluntarily break this hypothesis,
the plug-in produces proofs obligations that are impossible to lift:
-this kind of program cannot be analyzed with the value
-analysis plug-in.
+this kind of program cannot be analyzed with the EVA plug-in.
Here is an example of code that voluntarily breaks the base separation
hypothesis. Below is the same function written in the way it should
@@ -2513,34 +2518,34 @@ except that they come in two flavors:
Details about how to create and use these bases are provided in
section~\ref{malloc}.
-\section{What the value analysis does not provide}
+\section{What EVA does not provide}
\subsubsection{Values that are valid even if something bad happens}
-The value analysis provides sets of possible values under the
+EVA provides sets of possible values under the
assumption that the alarms emitted during the analysis have been
verified by the user (if necessary, using other techniques).
If during an actual execution of the application,
-one of the assertions emitted by the value analysis is violated,
-values other than those predicted by the value analysis may happen.
+one of the assertions emitted by EVA is violated,
+values other than those predicted by EVA may happen.
See also questions 2 and 3 in chapter \ref{faq}.
\subsubsection{Termination or reachability properties}
-Although the value analysis sometimes detects that
+Although EVA sometimes detects that
a function does not terminate, it cannot be used to prove that a
-function terminates. Generally speaking, the fact that the value
-analysis provides non-empty sets of values for a specific statement in
+function terminates. Generally speaking, the fact that EVA
+provides non-empty sets of values for a specific statement in
the application does not imply that this statement is reachable in a
-real execution. Currently, the value analysis is not designed to prove
+real execution. Currently, EVA is not designed to prove
the termination of loops or similar liveness properties.
For instance,
the following program does not terminate:
\listinginput{1}{termination.c}
If this program is analyzed
-with the default options of the value analysis, the analysis finds
+with the default options of EVA, the analysis finds
that every time execution reaches the end of \lstinline|main|, the value
of \lstinline|x| is in $\bropen 100..127\brclose$. This does
not mean that the function always terminates or even that it may
-sometimes terminate (it does neither). When the value analysis
+sometimes terminate (it does neither). When EVA
proposes an interval for \lstinline|x| at a point P,
it should always be interpreted as meaning
that {\em if P is reached, then at that time \lstinline|x| is in
@@ -2553,7 +2558,7 @@ do not come from a single propagated state but from the union of
several states that the analyzer may have propagated separately.
As a consequence, it should not be assumed that the ``state''
displayed at a particular program point has been propagated.
-In the following example, the value analysis did not emit any alarm
+In the following example, EVA did not emit any alarm
for the division at line 8. This means that the divisor was found never
to be null during an actual execution starting from the entry point.
The values displayed at the level of the comment should not be
@@ -2565,7 +2570,7 @@ int x, y, z;
main(int c){
...
...
-/* At this point the value analysis guarantees:
+/* At this point EVA guarantees:
x IN {0; 1}
y IN {0; 1}; */
z = 10 / (x - y);
@@ -2589,7 +2594,7 @@ propagated back to a particular call point. The only guarantee is
that the state that was propagated back to the call point is included
in the one displayed for the end of the function.
-The only way to be certain that the value analysis has propagated
+The only way to be certain that EVA has propagated
a specific state, and therefore guarantee the absence of run-time
errors under the assumptions encoded in that state, is to build
the intended state oneself, for instance with non-deterministic
@@ -2610,7 +2615,7 @@ looks like intended.
%\end{figure}
%\newpage
-{\em The value analysis is automatic but gives you a little bit of control.
+{\em EVA is automatic but gives you a little bit of control.
Just in case.}
\vspace{2cm}
@@ -2626,13 +2631,13 @@ frama-c-gui <options> <files>
Most parameters can also be set after the tool is launched,
in the graphical interface.
-The options understood by the value analysis plug-in are described in
+The options understood by the EVA plug-in are described in
this chapter. The files are the C files containing source code
to analyze.
For advanced users and plug-in developers, there exists
a ``batch'' version of Frama-C. The executable for the batch version is named
-\lstinline|frama-c| (or \lstinline|frama-c.exe|). All value analysis options
+\lstinline|frama-c| (or \lstinline|frama-c.exe|). All options of EVA
work identically for the GUI and batch version of Frama-C.
\bigskip
@@ -2642,7 +2647,7 @@ with short descriptions, from the command-line.
Option \lstinline|-kernel-help|
lists options that affect all plug-ins. Option
\lstinline|-value-help| lists options specific to the
-value analysis plug-in. The options \lstinline|-kernel-help| and
+EVA plug-in. The options \lstinline|-kernel-help| and
\lstinline|-value-help| also list advanced options that are
not documented in this manual.
@@ -2658,6 +2663,9 @@ $\dots$
$\dots$
\end{logs}
+The \lstinline|-val| prefix found in most options is historical, and stems
+from the former name of EVA (namely, Value).
+
\subsection{Analyzed files and preprocessing}\label{sec:analyz-files-prepr}
The analyzed files should be syntactically correct C. The files
@@ -2693,17 +2701,17 @@ frama-c-gui -val -cpp-command 'cat %1 > %2' file1.c file2.i
frama-c-gui -val -cpp-command 'CL.exe /C /E %1 > %2' file1.c file2.i
\end{shell}
-\subsection{Activating the value analysis}
+\subsection{Activating EVA}
-Option \lstinline|-val| activates the value analysis. Sets of
+Option \lstinline|-val| activates EVA. Sets of
values for the program's variables at the end of each analyzed function
are displayed on standard output.
-Many functionalities provided by Frama-C rely on the value analysis'
-results. Activating one of these automatically activates the value
-analysis, without it being necessary to provide the \lstinline|-val|
+Many functionalities provided by Frama-C rely on EVA's
+results. Activating one of these automatically activates EVA,
+without it being necessary to provide the \lstinline|-val|
option on the command-line. In this case, it should be kept in mind
-that all other value analysis options remain available for
+that all other options of EVA remain available for
parameterization.
\subsection{Saving the result of an analysis}
@@ -2801,7 +2809,7 @@ automatically generated includes the desired one. This may however
not always be the case. Even when it is the case, it is desirable
write an analysis entry point that positions the
values of \lstinline|argc| and \lstinline|argv| to
-improve the relevance of the alarms emitted by the value analysis.
+improve the relevance of the alarms emitted by EVA.
Although the above method is recommended for a complete
application, it remains possible to let the analysis automatically
@@ -2887,7 +2895,7 @@ The default value is 2. This number is the depth at which
additional variables named \lstinline|S_...| are allocated, so
two is plenty for most programs.
-For instance, here is the initial state displayed by the value analysis
+For instance, here is the initial state displayed by EVA
in \lstinline|-lib-entry| mode if a global variable \lstinline|s|
has type \lstinline|struct S| defined above:
\lstinputlisting[linerange={7-13}]
@@ -2899,7 +2907,7 @@ In this case, if variable \lstinline|s| is the only one which
is automatically allocated, it makes sense to set the option
\lstinline|-context-width| to one. The value of the
option \lstinline|-context-depth| represents the length of the
-linked list which is modelized with precision. After this depth,
+linked list which is modeled with precision. After this depth,
an imprecise value (called a well) captures all the possible continuations
in a compact but imprecise form.
@@ -2914,7 +2922,7 @@ with options \lstinline|-context-width 1|
In all the examples above, \lstinline|NULL| was one of the
possible values for all pointers, and the linked list that was
-modelized ended with a well that imprecisely captured all continuations
+modeled ended with a well that imprecisely captured all continuations
for the list. Also, the \lstinline|context-width| parameter
for the generated memory areas has to be understood as controlling the maximum
width for which the analyzer assumes the pointed area may be valid.
@@ -2952,12 +2960,12 @@ the hardware that computes floating-point operations. These modes
determine which arithmetic exceptions can be produced and rounding
direction for operations that are not exact.
-At this time, obtention of an
+At this time, obtaining an
infinite or NaN as result of a floating-point operation is always treated
as an unwanted error. Consequently, FPU modes related to arithmetic
exceptions are irrelevant for the analysis.
-The value analysis currently offers two modelizations of the
+EVA currently offers two models of the
floating-point hardware's rounding mode. Depending on the program analyzed
and the compiler used, one of the following situations may occur.
@@ -2966,7 +2974,7 @@ and the compiler used, one of the following situations may occur.
as if floating-point addition or multiplication were associative,
or transforms divisions into a multiplication by the inverse even when
the inverse cannot be represented exactly as a floating-point number.
-This case is not supported by the value analysis.
+This case is not supported by EVA.
\item The program uses only
\lstinline|double| and \lstinline|float| floating-point types,
@@ -2974,7 +2982,7 @@ does not change the default (nearest-even) floating-point rounding
mode and is compiled with a compiler that neither generates
\lstinline|fmadd| instructions nor generates extended precision computations
(historical x87 instruction set). It can be analyzed with the default
-modelization of floating-point rounding.
+modeling of floating-point rounding.
\item The program uses only
\lstinline|double| and \lstinline|float| floating-point types,
@@ -3019,10 +3027,10 @@ analyzed application. If this is not possible, the analysis can also be
parameterized manually with the characteristics of the target
architecture.
-\subsection{Parameterizing the modelization of the C language}
+\subsection{Parameterizing the modeling of the C language}
The following options are more accurately described as
-pertaining to Frama-C's modelization of the C language
+pertaining to Frama-C's modeling of the C language
than as a description of the target platform, but of course
the distinction is not always clear-cut. The important thing to remember
is that these options, like the previous one, are dangerous options
@@ -3030,7 +3038,7 @@ that should be used, or omitted, carefully.
\subsubsection{Valid absolute addresses in memory}
-By default, the value analysis assumes that the absolute addresses in
+By default, EVA assumes that the absolute addresses in
memory are all invalid. This assumption can be too restrictive,
because in some cases there exist a limited number of absolute
addresses which are intended to be accessed by the analyzed program,
@@ -3047,27 +3055,27 @@ in a future version.
\subsubsection{Overflow in array accesses}
\label{unsafe-arrays}
-The value analysis assumes that when an array
+EVA assumes that when an array
access occurs in the analyzed program, the intention is that the
accessed address should be inside the array. If it can not determine that
this is the case, it emits an \lstinline|out of bounds index|
alarm. This leads to an alarm on the following example:
\lstinputlisting[numbers=left]
{examples/parametrizing/out-of-bound.c}
-The value analysis assumes that writing \lstinline|t[0][...]|, the programmer
+EVA assumes that writing \lstinline|t[0][...]|, the programmer
intended the memory access to be inside \lstinline|t[0]|. Consequently,
it emits an alarm:
\lstinputlisting[linerange={8-8},breaklines=true]
{examples/parametrizing/out-of-bound.log}
-The option \lstinline|-unsafe-arrays| tells the value analysis to warn
-only if the address as computed using its modelization of pointer arithmetics
-is invalid. With the option, the value analysis does not warn about line 4
+The option \lstinline|-unsafe-arrays| tells EVA to warn
+only if the address as computed using its modeling of pointer arithmetics
+is invalid. With the option, EVA does not warn about line 4
and assumes that the programmer
was referring to the cell \lstinline|t[1][2]|.
The default behavior is stricter than necessary but often produces more
readable and useful alarms. To reiterate, in this default behavior
-the value analysis gets hints from the syntactic shape of the program.
+EVA gets hints from the syntactic shape of the program.
Even in the default mode, it does not warn for the following code.
\begin{listing}{4}
int *p=&t[0][12];
@@ -3079,7 +3087,7 @@ Option \lstinline|-safe-arrays| also has an effect on the evaluation
of the ACSL construct ``\lstinline|..|''. When \lstinline|t| is a
known array, \lstinline|t[..]| is strictly equivalent to
\lstinline|t[0..s-1]|, where \lstinline|s| is the number of elements
-of \lstinline|t|. Conversely, when option \lstinline|-usafe-arrays| is
+of \lstinline|t|. Conversely, when option \lstinline|-unsafe-arrays| is
set, \lstinline|t[..]| means
\lstinline|t[-|$\infty$\lstinline|..+|$\infty$\lstinline|]| -- meaning
that the location overlaps with neighbouring zones when \lstinline|t| is
@@ -3087,7 +3095,7 @@ inside an array or struct.
\subsection{Dealing with library functions}
-When the value analysis plug-in encounters a call to a library
+When the EVA plug-in encounters a call to a library
function, it may need to make assumptions about the effects of this call.
The behavior of library functions can be described precisely
by writing a contract for the function (chapter \ref{annotations}),
@@ -3104,7 +3112,7 @@ contract should be verified carefully by the user.
\section{Controlling approximations}
Unlike options of section \ref{context}, which used wrongly may cause
-the value analysis to produce incorrect results, all the options
+EVA to produce incorrect results, all the options
in this section give the user control over the tradeoff between the
quality of the results and the resources taken by the analyzer to
provide them. The options described in this section can, so to speak,
@@ -3221,7 +3229,7 @@ Example:
\subsubsection{Loop unrolling}\label{deroulage}
-There are two different options for forcing the value analysis
+There are two different options for forcing EVA
to unroll the effects of the body of the loop, as many times as
specified, in order to obtain a precise representation of the effects
of the loop itself. If the number of iterations is sufficient,
@@ -3367,11 +3375,11 @@ of \lstinline+-slevel+ or \lstinline+-ulevel+,
the technique above does not unroll the loop; thus the overall results
are less precise, but the analysis can be faster.
-Notice that, in the fonction above, a more precise loop invariant would be
+Notice that, in the function above, a more precise loop invariant would be
\begin{listing}{5}
/*@ loop invariant p < &t[c-1]; */
\end{listing}
-However, this annotation cannot be effectively used by the value analysis
+However, this annotation cannot be effectively used by EVA
if the value for \lstinline+c+ is imprecise, which is the case in our
example. As a consequence, the analysis cannot prove this improved invariant.
We have effectively replaced an alarm, the possible out-of-bounds access at
@@ -3390,7 +3398,7 @@ if \lstinline|f| contains large/nested loops, significant
time may be spent recording the values taken by the program's variables
at each of \lstinline|f|'s statements.
If the user knows that these values will not be useful later,
-ey can instruct the value analysis not to record these with the
+ey can instruct EVA not to record these with the
\lstinline|-no-results-function f| option.
The \lstinline|-no-results-function| option
can be used several times, to omit the results of several functions.
@@ -3428,8 +3436,8 @@ time frama-c -val nor.c -slevel 2001 -no-results-function irrelevant_function
When instructed, with
option \lstinline|-no-results-function irrelevant_function|,
that the values for the function
-\lstinline|irrelevant_function| do not need to be kept, the value
-analysis takes less than a second to produce its results. This shows
+\lstinline|irrelevant_function| do not need to be kept, EVA
+takes less than a second to produce its results. This shows
that in the earlier analysis, most of the time was not spent in the
analysis itself but in recording the values
of \lstinline|irrelevant_function|.
@@ -3477,17 +3485,17 @@ reads and writes.
Alternatively, one can leave the body of the function untouched, but
still write a contract. Then it is possible to use the option
-\verb+-val-use-spec f+. This instructs the value analysis to use the
+\verb+-val-use-spec f+. This instructs EVA to use the
specification of \verb+f+ instead of its body each time a call to
\verb+f+ is encountered. This is equivalent\footnote{Except for a few
properties, as described in the next paragraph.} to deleting the body
-of \verb+f+ for the value analysis, but not for the other plug-ins of \FramaC,
+of \verb+f+ for EVA, but not for the other plug-ins of \FramaC,
that may study the body of \verb+f+ on their own.
Notice that option \verb+-val-use-spec f+ loses some guarantees. In particular,
-the body of \verb+f+ is not studied at all by the value analysis. Neither
+the body of \verb+f+ is not studied at all by EVA. Neither
are the functions that \verb+f+ calls, unless they are used by some other
-functions than \verb+f+. Moreover, the value analysis does not attempt
+functions than \verb+f+. Moreover, EVA does not attempt
to check that \verb+f+ conforms to its specification. In particular,
postconditions are marked as {\em unknown} with \verb+-val-use-spec+,
while they are {\em considered valid} for functions without body.
@@ -3517,16 +3525,20 @@ analysis of the program shows a correct but approximated result:
{examples/parametrizing/ilevel.1.log}
Studying the program, the user may decide to improve the precision of
-the result by adding \verb|-val-ilevel 16| to the commandline. The
+the result by adding \verb|-val-ilevel 16| to the command line. The
analysis result then becomes:
\lstinputlisting[linerange={28-30}]
{examples/parametrizing/ilevel.2.log}
+\section{Advanced analyses}
+\label{sec:eva}
+
+\emph{To be written}
\section{Non-termination}
-The parameterization of the value analysis can lead to situations where the
+The parameterization of EVA can lead to situations where the
analysis stops abruptly due to the absence of valid states. For instance,
some primitives (section \ref{primitives}) may detect an invalid
precondition and stop propagating the current callstack, or a loop may
@@ -3539,18 +3551,18 @@ of possibly false alarms. However, priority should be given to these
alarms, since they are likely to indicate an incorrect parameterization.
To help identify these situations, the {\em Nonterm} plug-in has been
-developed. It runs after the value analysis, by adding \verb|-then -nonterm|
+developed. It runs after EVA, by adding \verb|-then -nonterm|
at the end of the command-line.
{\em Nonterm} emits warnings about non-terminating instructions in functions
-analyzed by Value. It operates on a per-callstack basis, and therefore
+analyzed by EVA. It operates on a per-callstack basis, and therefore
displays more precise results than a visual inspection on the GUI;
in particular, if there are both terminating and non-terminating callstacks for
a given statement, the GUI will not color their successors red
(because of the terminating callstacks), but {\em Nonterm} will emit warnings
for the non-terminating ones.
-{\em Nonterm} only reports situations where the value analysis is able to
+{\em Nonterm} only reports situations where EVA is able to
guarantee non-termination. Because its purpose is to prioritize warnings
that are likely to indicate parameterization errors,
it does not consider callstacks where termination seems possible.
@@ -3579,7 +3591,7 @@ amount of warnings and is rarely needed in practice.
{\em Frama-C can compute and display the inputs (memory locations read from),
outputs (memory locations written to),
and precise dependencies between outputs and inputs,
-for each function. These computations use the value analysis
+for each function. These computations use EVA
for resolving array indices and pointers.}
\vspace{2cm}
@@ -3751,7 +3763,7 @@ guarantees that initializing \lstinline|a| is unnecessary.
{\em Frama-C's language for annotations is ACSL. Only a subset
of the properties that can be expressed in ACSL can effectively
-be of service to or be checked by the value analysis plug-in.}
+be of service to or be checked by the EVA plug-in.}
\vspace{2cm}
@@ -3793,7 +3805,7 @@ The analysis log contains property statuses relative to the state
currently propagated (this is to help the user understand the
conditions in which the property fails to verify). The same property
can appear several times in the log, for instance if its truth value is
-\lstinline|valid| for some passages of the value analysis and
+\lstinline|valid| for some passages of EVA and
\lstinline|invalid| for others.\footnote{Conversely, as Frama-C's
logging mechanism suppresses the printing of identical message,
the property is printed only once with each status.}
@@ -3822,7 +3834,7 @@ Let us consider for instance the following function.
frama-c -val -slevel 12 -lib-entry -main f reduction.c
\end{shell}
-The value analysis emits the following two warnings:
+EVA emits the following two warnings:
\begin{logs}
reduction.c:8: warning: Assertion got status unknown.
reduction.c:8: warning: Assertion got status valid.
@@ -3879,7 +3891,7 @@ not been an annotation. It cannot make the state more general. For instance,
it is not possible to use a precondition to add more aliasing in
an initial state generated by option \lstinline|-lib-entry|,
because it would be a generalization, as opposed to a restriction;
-\item the interpretation of an ACSL formula by the value analysis may be
+\item the interpretation of an ACSL formula by EVA may be
approximated. The state effectively used after taking the annotation
into account is a superset of
the state described by the user. In the worst case (for instance if
@@ -3935,7 +3947,7 @@ Then:
the next postcondition, using state $A$.
\item If $\mathcal{V}$ is \lstinline|unknown|, the postcondition may
- be invalid for some states $A_I \subset A$. The analyzer attemps to reduce
+ be invalid for some states $A_I \subset A$. The analyzer attempts to reduce
$A$ according to $P$, as explained in section~\ref{reduction_proprietes}.
The resulting state $A_V$ is used to evaluate the subsequent postconditions.
Notice that $P$ does \emph{not} necessarily hold in $A_V$, as reduction is not
@@ -3998,11 +4010,11 @@ void withdraw(purse *p,int s) {
\paragraph{Direct and indirect from clauses}
-Value makes use of specifications that are more precise than the ACSL
+EVA makes use of specifications that are more precise than the ACSL
language specifies in that it establishes a distinction between
\emph{direct} and \emph{indirect} dependencies. A dependency is direct
if the value contained in the dependency impacts the value of the
-lvalue refered to in the assign clause; a dependency is indirect if
+lvalue referred to in the assign clause; a dependency is indirect if
the value is used only in a conditional or to compute an address. Indirect
dependencies are distinguished by an ``indirect'' label; other
dependencies are direct. See for instance the valid ACSL contract
@@ -4027,7 +4039,7 @@ project. This happens when the function is really not available
because it did something that was complicated and unimportant
for the analysis at hand.
-The value analysis uses the \lstinline|assigns| clauses provided for
+EVA uses the \lstinline|assigns| clauses provided for
library functions. It does not take advantage of the
\lstinline|assigns| clauses of functions whose implementation is also
available, except when option \lstinline|-val-use-spec| is used
@@ -4055,7 +4067,7 @@ are modelled by the analyzer as follows:
the values present at $l$ in $S$, but also $v'$. This reflects the
fact that $l$ \emph{may} have been overwritten.
-\item furthemore, if \lstinline|loc| and \lstinline|locD| are
+\item furthermore, if \lstinline|loc| and \lstinline|locD| are
distinct locations in $S$, the locations in $L$ are updated to
contain \emph{exactly} $v'$. Indeed, in this case, \lstinline|loc| is
necessarily overwritten.\footnote{A correct assigns clause for a function
@@ -4064,7 +4076,7 @@ are modelled by the analyzer as follows:
\end{enumerate}
Notice that the values written in \lstinline|loc1| are \emph{entirely}
-determined by \lstinline|locD| and $S$. The value analysis does not attempt
+determined by \lstinline|locD| and $S$. EVA does not attempt
to ``invent'' generic values, and it is very important to write
\lstinline|\from| clauses that are sufficiently broad to encompass all
the real behaviors of the function.
@@ -4093,7 +4105,7 @@ please contact the developers.
\paragraph{Postconditions of library functions}
-When evaluating a function contract, the value analysis handles the
+When evaluating a function contract, EVA handles the
evaluation of a postcondition in two different ways, depending on
whether the function $f$ being evaluated has a source body or just a
specification.
@@ -4116,7 +4128,7 @@ specification.
of~$f$.
%
Then, since postconditions cannot be proven correct without a
- body, they are \emph{assumed} correct, and the value analysis does not
+ body, they are \emph{assumed} correct, and EVA does not
compute their truth values. Accordingly, no truth value is output on the
analysis log, except when we suspect the postcondition of being
incorrect.
@@ -4152,7 +4164,7 @@ int succ(int x);
Similarly, forgetting the \lstinline|\from| clause in the contract
for \lstinline|g| would stop the evaluation (without knowing where
- the value of \lstinline|p| comes from, \textsc{Value} assumes that
+ the value of \lstinline|p| comes from, EVA assumes that
it points to a constant address).
\begin{listing}{1}
@@ -4218,7 +4230,7 @@ The source code for these functions is not necessarily available, as
they are part of the system rather than of the application itself. In
theory, it would be possible for the user to give a C implementation
of these functions, but those implementations might prove difficult to
-analyze for the value analysis plug-in. A more pragmatic solution is to use a
+analyze for the EVA plug-in. A more pragmatic solution is to use a
primitive function of the analyzer for each standard library call that
would model as precisely as possible the effects of the call.
@@ -4235,7 +4247,7 @@ string functions (e.g. \lstinline|strlen| and \lstinline|strnlen|),
some floating-point mathematical functions (e.g. \lstinline|sin| and
\lstinline|pow|), and functions for dynamic memory allocation
(\lstinline|malloc|, \lstinline|realloc| and \lstinline|free|)%
-The complete list of builtins for the value analysis (including builtins
+The complete list of builtins for EVA (including builtins
unrelated to the standard C library) is presented in
section~\ref{builtins-list}.
@@ -4306,7 +4318,7 @@ are guaranteed to occur a finite number of times.
Option \lstinline|-val-mlevel| (default 0) sets the maximum number of calls to
\lstinline|malloc| (and similar functions) per call stack for which the
weak version of the builtins will return a precise fresh location.
-Aterwards, the locations will be reused to ensure termination of the analysis --
+Afterwards, the locations will be reused to ensure termination of the analysis --
but leading to spurious aliasing and possible imprecision.
In other words, setting \lstinline|-val-mlevel N| means that up to $N+1$
different locations will be created for each call stack. This allows,
@@ -4315,7 +4327,7 @@ termination for other loops.
\paragraph{Memory allocation failure}
-By default, the memory allocation builtins in the value analysis consider that
+By default, the memory allocation builtins in EVA consider that
the allocation may fail, thus \lstinline|NULL| is always returned as a possible
value. To change this behavior (supposing that these functions never fail),
use option \lstinline|-no-val-malloc-returns-null|.
@@ -4329,7 +4341,7 @@ use option \lstinline|-no-val-malloc-returns-null|.
The following functions, declared in \lstinline|share/libc/__fc_builtin.h|, allow to
introduce some non-determinism in the analysis. The results given by
-the value analysis are
+EVA are
valid \textbf{for all values proposed by the user}, as opposed
to what a test-generation tool would typically do. A tool based
on testing techniques
@@ -4424,7 +4436,7 @@ void f(int x)
\section{Table of builtins}
\label{builtins-list}
-This table briefly summarizes all builtins present in the value analysis, with
+This table briefly summarizes all builtins present in EVA, with
a short description of their behavior.
\subsection{Floating-point operations}
@@ -4551,7 +4563,7 @@ They are listed here for completeness.
\subsection{Operations on the abstract state}
These builtins perform low-level operations on the abstract representation
-manipulated internally by Value Analysis. Usually not for the casual user.
+manipulated internally by EVA. Usually not for the casual user.
\begin{itemize}
\item \lstinline|Frama_C_dump_assert_each| prints the abstract state as an
@@ -4653,7 +4665,7 @@ Consider the following example:
\listinginput{1}{vraie_al.c}
-When analyzing this example, the value analysis does not emit an
+When analyzing this example, EVA does not emit an
alarm on line 6. This is perfectly correct, since no error occurs at
run time on line 6. In fact, line 6 is not reached at all, since
execution stops at line 5 when attempting to dereference
@@ -4672,8 +4684,8 @@ or the absence thereof (see next question).
information to the tool so that it detects these alarms?}
The answers to these questions are respectively ``yes'' and
-``there is nothing special to do''. If an alarm might be spurious, the
-value analysis automatically goes on. If the alarm is really a
+``there is nothing special to do''. If an alarm might be spurious, EVA
+automatically goes on. If the alarm is really a
false alarm, the result given in the rest of the analysis can be
considered with the same level of trust than if Frama-C had not
displayed the false alarm. One should however keep in mind
diff --git a/opam/opam b/opam/opam
index 260ad29a3fde7a99b518534ea6d72a27bf460aa7..1ddb09a5a64124e95040c4bf63afffa22ce83009 100644
--- a/opam/opam
+++ b/opam/opam
@@ -31,7 +31,7 @@ authors: [
]
homepage: "http://frama-c.com/"
license: "GNU Lesser General Public License version 2.1"
-dev-repo: "https://github.com/Frama-C/Frama-C-snapshot.git#release-candidates"
+dev-repo: "https://github.com/Frama-C/Frama-C-snapshot.git"
doc: ["http://frama-c.com/download/user-manual-Aluminium-20160501.pdf"]
bug-reports: "https://bts.frama-c.com/"
tags: [
diff --git a/src/kernel_internals/typing/cabs2cil.mli b/src/kernel_internals/typing/cabs2cil.mli
index cec2ca14275de43cf46a5e63080e3d4c8d076d79..129621b02ca0e2a6d0b65cf94b032f6a8389c84d 100644
--- a/src/kernel_internals/typing/cabs2cil.mli
+++ b/src/kernel_internals/typing/cabs2cil.mli
@@ -75,7 +75,7 @@ val register_new_global_hook: (Cil_types.varinfo -> bool -> unit) -> unit
corresponding to the global, while the boolean is [true] iff [vi] was
already existing (it is [false] if this is the first declaration/definition
of [vi] in the file).
- @since Frama-C+dev
+ @since Silicon-20161101
*)
(** new hook called when encountering a definition of a local function. The hook
diff --git a/src/kernel_services/analysis/stmts_graph.mli b/src/kernel_services/analysis/stmts_graph.mli
index 88d783b5c0506acdb5fb8e5ba3e35f1b3be06a4a..dcc8972616e175afd1bd372fb787073b3d8db2cb 100644
--- a/src/kernel_services/analysis/stmts_graph.mli
+++ b/src/kernel_services/analysis/stmts_graph.mli
@@ -50,7 +50,7 @@ val stmt_is_in_cycle_filtered : (stmt -> bool) -> stmt -> bool
Note that this function is not tail-recursive and may not work with
very large graphs.
- @modify Aluminium-20160501+dev return type changed to hptset *)
+ @modify Silicon-20161101 return type changed to hptset *)
val reachable_stmts: kernel_function -> stmt -> Stmt.Hptset.t
(** Get the statements that compose [s]. For a simple statement (not containing
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 684249b36915abe36bccb64092b1f44de47b6ed8..331057aef902514fb62f45babc56561d86766519 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -1656,7 +1656,7 @@ and code_annotation_node =
| APragma of term pragma (** pragma. *)
| AExtended of string list * acsl_extension
(** extension in a loop annotation.
- @since Frama-C+dev *)
+ @since Silicon-20161101 *)
(** function contract. *)
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 489e51982beda75ee2a1ab7530b649f6bb1875df..97fccc8563931c5022545499a9d7d386ff487408 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1699,7 +1699,7 @@ end
@plugin development guide
@since Sodium-20150201
- @modify Frama-C+dev
+ @modify Silicon-20161101
*)
val register_behavior_extension:
string ->
@@ -1847,7 +1847,7 @@ val visitCilBehaviors: cilVisitor -> funbehavior list -> funbehavior list
(** visit an extended clause of a behavior.
@since Nitrogen-20111001
- @modify Frama-C+dev
+ @modify Silicon-20161101
*)
val visitCilExtended: cilVisitor -> acsl_extension -> acsl_extension
diff --git a/src/kernel_services/ast_queries/file.mli b/src/kernel_services/ast_queries/file.mli
index 6fbfe7c7239e4863c41f594dfe74ec5645a87645..caa69b6f7c7883442f334d8587e406692ee73ac7 100644
--- a/src/kernel_services/ast_queries/file.mli
+++ b/src/kernel_services/ast_queries/file.mli
@@ -116,7 +116,7 @@ val add_code_transformation_after_cleanup:
val constfold: code_transformation_category
(** category for syntactic constfolding (done after cleanup)
- @since Frama-C+dev *)
+ @since Silicon-20161101 *)
val must_recompute_cfg: Cil_types.fundec -> unit
(** [must_recompute_cfg f] must be called by code transformation hooks
diff --git a/src/kernel_services/ast_queries/filecheck.mli b/src/kernel_services/ast_queries/filecheck.mli
index a278ae33460654b507780bb2cf348babbf781596..3e70a8deb0222f88fb6d6513deaff6236be96c62 100644
--- a/src/kernel_services/ast_queries/filecheck.mli
+++ b/src/kernel_services/ast_queries/filecheck.mli
@@ -31,7 +31,7 @@ val check_ast: ?is_normalized:bool -> ?ast:Cil_types.file -> string -> unit
Note that the check is only partial.
@since Aluminium-20160501
- @modify Frama-C+dev adds optional ast argument
+ @modify Silicon-20161101 adds optional ast argument
*)
(*
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index 1d045591a3613fa8e571e9aed35b8c41db0f9513..61bdd0a9c3fb01937b265d37286c53ba2394188a 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -130,7 +130,7 @@ type typing_context = {
@plugin development guide
@since Carbon-20101201
- @modify Frama-C+dev change type of the function
+ @modify Silicon-20161101 change type of the function
*)
val register_behavior_extension:
string ->
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index 3bbd5f1e097890d7e25852ac0acc898e3dd8922f..2dab98708f0db1c3224df0758ad1e1011f74821a 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -390,7 +390,7 @@ val constFoldTermToInt: ?machdep:bool -> term -> Integer.t option
Requires a mapping from [varinfo] to [init option]
(e.g. based on [Globals.Vars.find]).
- @since Aluminium-20160501+dev
+ @since Silicon-20161101
*)
class simplify_const_lval: (varinfo -> init option) -> Cil.cilVisitor
diff --git a/src/kernel_services/cmdline_parameters/cmdline.mli b/src/kernel_services/cmdline_parameters/cmdline.mli
index 917312c81411a3cac7b140933e14205f16bf70f1..95f0fb8ccd39b194b3c51cd3c9fdd8af108f4f25 100644
--- a/src/kernel_services/cmdline_parameters/cmdline.mli
+++ b/src/kernel_services/cmdline_parameters/cmdline.mli
@@ -392,7 +392,7 @@ val load_all_plugins: (unit -> unit) ref
val add_loading_failures: string -> unit
(** Add a package to the list of ocamlfind packages that have failed to be
loaded.
- @since Frama-C+dev *)
+ @since Silicon-20161101 *)
(**/**)
diff --git a/src/kernel_services/cmdline_parameters/parameter_sig.mli b/src/kernel_services/cmdline_parameters/parameter_sig.mli
index 57925329ac6db025ffac0ecc9ea8a3d53614e43b..cbbd63f5f31545deb803d468a6ed9ed7cdda8ca3 100644
--- a/src/kernel_services/cmdline_parameters/parameter_sig.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_sig.mli
@@ -340,7 +340,7 @@ module type Collection_category = sig
val all: unit -> t
(** The '\@all' category. If this category has not been created, it is
{!none}, which means 'ignored'.
- @since Frama-C+dev *)
+ @since Silicon-20161101 *)
val set_default: t -> unit
(** Modify the '\@default' category. *)
diff --git a/src/kernel_services/parsetree/logic_ptree.mli b/src/kernel_services/parsetree/logic_ptree.mli
index 3b8dff948c889d6902cbecaa94aafa5014341c97..f76476fa6ebe8c50a1b6cec8be010ebfc6ecd20e 100644
--- a/src/kernel_services/parsetree/logic_ptree.mli
+++ b/src/kernel_services/parsetree/logic_ptree.mli
@@ -314,7 +314,7 @@ type code_annot =
| APragma of lexpr Cil_types.pragma (** pragma. *)
| AExtended of string list * extension
(** extension in a loop annotation.
- @since Frama-C+dev *)
+ @since Silicon-20161101 *)
(** assignment performed by a C function. *)
type assigns = lexpr Cil_types.assigns
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index dd5b0e976d266679def3198b751bada225e14a1a..830834a4282777e1ca4da09617e73b556765e25e 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -375,7 +375,7 @@ module Time =
let () = Parameter_customize.is_invisible ()
let () = Parameter_customize.set_negative_option_name "-do-not-collect-messages"
let () = Parameter_customize.do_not_projectify ()
-module Collect_messages = (* TODO: remove in Silicium *)
+module Collect_messages = (* TODO: remove in Silicon *)
Bool
(struct
let module_name = "Collect_messages"
diff --git a/src/kernel_services/plugin_entry_points/plugin.mli b/src/kernel_services/plugin_entry_points/plugin.mli
index 344422432d59b0d6ea28bd8b74238fed4c5ea096..f7975983b43fabc733a0f65f5e4c7b117a6737d7 100644
--- a/src/kernel_services/plugin_entry_points/plugin.mli
+++ b/src/kernel_services/plugin_entry_points/plugin.mli
@@ -126,7 +126,7 @@ val plugin_subpath: string -> unit
val default_msg_keys: string list -> unit
(** Debug message keys set by default for the plugin.
- @since Frama-C+dev *)
+ @since Silicon-20161101 *)
(* ************************************************************************* *)
(** {2 Handling plugins} *)
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index c76398aff95fd9565b93932eea046e628190d700..53e533497e003d1368f2e40334d6a709728714e6 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -353,7 +353,7 @@ val usleep: int -> unit
external compare_basic: 'a -> 'a -> int = "%compare"
(** Case-insensitive string comparison. Only ISO-8859-1 accents are handled.
- @since Frama-C+dev *)
+ @since Silicon-20161101 *)
val compare_ignore_case: string -> string -> int
(*
diff --git a/src/libraries/utils/command.mli b/src/libraries/utils/command.mli
index 79fa9306a0e5c6c583e70a88bec94e920ea4c47a..f3b5e1dba4c0d273b9d7289c30098e0f8bddc09c 100644
--- a/src/libraries/utils/command.mli
+++ b/src/libraries/utils/command.mli
@@ -42,7 +42,7 @@ val bincopy : bytes -> in_channel -> out_channel -> unit
and copy it in [cout].
[buffer] is a temporary string used during the copy.
Recommanded size is [2048].
- @modify Frama-C+dev [buffer] has now type [bytes] instead of [string]
+ @modify Silicon-20161101 [buffer] has now type [bytes] instead of [string]
*)
val copy : string -> string -> unit
diff --git a/src/libraries/utils/pretty_utils.mli b/src/libraries/utils/pretty_utils.mli
index 5ee9ce35172150f162dbf047b6417592b2459871..c24d61b4a52057ca2a1f16f316b20b0e657ffcc4 100644
--- a/src/libraries/utils/pretty_utils.mli
+++ b/src/libraries/utils/pretty_utils.mli
@@ -29,7 +29,7 @@
val sfprintf: ('a,Format.formatter,unit,string) format4 -> 'a
(** Equivalent to Format.asprintf. Used for compatibility with OCaml < 4.01.
- @deprecated Aluminium-20160501+dev use Format.asprintf *)
+ @deprecated Silicon-20161101 use Format.asprintf *)
val ksfprintf:
(string -> 'b) -> ('a, Format.formatter, unit, 'b) format4 -> 'a
@@ -67,7 +67,7 @@ val pp_list: ?pre:sformat -> ?sep:sformat -> ?last:sformat -> ?suf:sformat ->
- the suffix to output after a non-empty list (default: close box)
- what to print if the list is empty (default: nothing)
- @modify Aluminium-20160501+dev new optional argument [empty]
+ @modify Silicon-20161101 new optional argument [empty]
*)
val pp_array: ?pre:sformat -> ?sep:sformat -> ?suf:sformat -> ?empty:sformat ->
@@ -78,7 +78,7 @@ val pp_array: ?pre:sformat -> ?sep:sformat -> ?suf:sformat -> ?empty:sformat ->
- the suffix to output after a non-empty array (default: close box)
- what to print if the array is empty (default: nothing)
- @modify Aluminium-20160501+dev new optional argument [empty]
+ @modify Silicon-20161101 new optional argument [empty]
*)
val pp_iter:
@@ -106,7 +106,7 @@ val pp_opt: ?pre:sformat -> ?suf:sformat -> ?none:sformat -> 'a formatter -> 'a
(** pretty-prints an optional value. Prefix and suffix default to "@[" and "@]"
respectively. If the value is [None], pretty-print using [none].
- @modify Aluminium-20160501+dev new optional argument [none] *)
+ @modify Silicon-20161101 new optional argument [none] *)
val pp_cond: ?pr_false:sformat -> bool -> sformat formatter
(** [pp_cond cond f s] pretty-prints [s] if cond is [true] and the optional
diff --git a/src/plugins/value/domains/cvalue/builtins.mli b/src/plugins/value/domains/cvalue/builtins.mli
index 636dd4613eb81b862a0478a82cc2d9bac999d694..dd3bfc879c2d5cee854768535f89dff4d718ba8e 100644
--- a/src/plugins/value/domains/cvalue/builtins.mli
+++ b/src/plugins/value/domains/cvalue/builtins.mli
@@ -55,7 +55,7 @@ val clobbered_set_from_ret: Cvalue.Model.t -> Cvalue.V.t -> Base.SetLattice.t
[kind] is used to describe the alarm, similarly to [Alarms.get_name].
Identical alarms are not re-emitted. Returns [true] iff it is a new alarm.
- @modify Aluminium-20160501+dev change return type *)
+ @modify Silicon-20161101 change return type *)
val emit_alarm: kind:string -> text:string -> bool
(** Iteration on special assertions built by the builtins *)
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 336fc9d84704e4304099d8435333ad7e1178f9dd..8be2acc73c8976ccfc9c2a4763c02e9abb0373e7 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -947,7 +947,7 @@ module ValShowInitialState =
True
(struct
let option_name = "-val-show-initial-state"
- (* deprecated in Silicium *)
+ (* deprecated in Silicon *)
let help = "[deprecated] Show initial state before analysis starts. \
This option has been replaced by \
-val-msg-key=[-]initial-state and has no effect anymore."
diff --git a/src/plugins/value_types/widen_type.mli b/src/plugins/value_types/widen_type.mli
index d6eb28d2dbd8201f5d498fa282d5aa52863abd09..380676b76dd7f169b4d2120aba3cd0d00bc60756 100644
--- a/src/plugins/value_types/widen_type.mli
+++ b/src/plugins/value_types/widen_type.mli
@@ -33,7 +33,7 @@ val default : unit -> t
val join: t -> t -> t
(** Pretty-prints a set of hints (for debug purposes only).
- @since Aluminium-20160501+dev *)
+ @since Silicon-20161101 *)
val pretty : Format.formatter -> t -> unit
(** Define numeric hints for one or all variables ([None]),
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 1e3d90db29b2b47b5caabcaea357848563b7752f..30364739d4d43787e13e461b2155570fa2230446 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -22,7 +22,7 @@
###############################################################################
################################
-Plugin WP 1.1 Silicium_20161101
+Plugin WP 1.1 Silicon_20161101
################################
- WP [2016/04/08] Unified variable usage for all models
diff --git a/src/plugins/wp/doc/manual/frama-c-book.cls b/src/plugins/wp/doc/manual/frama-c-book.cls
deleted file mode 100644
index 01090add59fe2cde8650632031cd210c718e49d3..0000000000000000000000000000000000000000
--- a/src/plugins/wp/doc/manual/frama-c-book.cls
+++ /dev/null
@@ -1,345 +0,0 @@
-% --------------------------------------------------------------------------
-% --- LaTeX Class for Frama-C Books ---
-% --------------------------------------------------------------------------
-\NeedsTeXFormat{LaTeX2e}
-\ProvidesPackage{frama-c-book}[2009/02/05 LaTeX Class for Frama-C Books]
-% --------------------------------------------------------------------------
-% --- Base Class management ---
-% --------------------------------------------------------------------------
-\LoadClass[a4paper,11pt,twoside,openright]{report}
-\DeclareOption{web}{\PassOptionsToPackage{colorlinks,urlcolor=blue}{hyperref}}
-\DeclareOption{paper}{\PassOptionsToPackage{pdfborder=0 0 0}{hyperref}}
-\ProcessOptions
-\RequirePackage{fullpage}
-\RequirePackage{ifthen}
-\usepackage{lmodern}
-\RequirePackage[T1]{fontenc}
-\RequirePackage[utf8]{inputenc}
-\RequirePackage[pdftex,pdfstartview=FitH]{hyperref}
-\RequirePackage{amssymb}
-\RequirePackage{xcolor}
-\RequirePackage[pdftex]{graphicx}
-\RequirePackage{xspace}
-\RequirePackage{makeidx}
-\RequirePackage[leftbars]{changebar}
-\RequirePackage[english]{babel}
-\RequirePackage{fancyhdr}
-\RequirePackage{titlesec}
-\RequirePackage{upquote}
-% --------------------------------------------------------------------------
-% --- Page Layout ---
-% --------------------------------------------------------------------------
-\setlength{\voffset}{-6mm}
-\setlength{\headsep}{8mm}
-\setlength{\footskip}{21mm}
-\setlength{\textheight}{238mm}
-\setlength{\topmargin}{0mm}
-\setlength{\textwidth}{155mm}
-\setlength{\oddsidemargin}{2mm}
-\setlength{\evensidemargin}{-2mm}
-\setlength{\changebarsep}{0.5cm}
-\setlength{\headheight}{13.6pt}
-\def\put@bg(#1,#2,#3)#4{\setlength\unitlength{1cm}%
- \begin{picture}(0,0)(#1,#2)
- \put(0,0){\includegraphics[width=#3cm]{#4}}
- \end{picture}}
-\fancypagestyle{plain}{%
- \fancyfoot{}
- \fancyhead{}
- \fancyhead[LE]{\put@bg(2.4,27.425,21){frama-c-left.pdf}}
- \fancyhead[LO]{\put@bg(2.7,27.425,21){frama-c-right.pdf}}
- \fancyhead[CE]{\scriptsize\textsf{\leftmark}}
- \fancyhead[CO]{\scriptsize\textsf{\rightmark}}
- \fancyfoot[C]{\small\textsf{\thepage}}
- \renewcommand{\headrulewidth}{0pt}
- \renewcommand{\footrulewidth}{0pt}
-}
-\fancypagestyle{blank}{%
- \fancyfoot{}
- \fancyhead{}
- \fancyhead[LE]{\put@bg(2.4,27.425,21){frama-c-left.pdf}}
- \fancyhead[LO]{\put@bg(2.7,27.425,21){frama-c-right.pdf}}
-}
-%% Redefinition of cleardoublepage for empty page being blank
-\def\cleardoublepagewith#1{\clearpage\if@twoside \ifodd\c@page\else
-\hbox{}
-\thispagestyle{#1}
-\newpage
-\fi\fi}
-\def\cleardoublepage{\cleardoublepagewith{blank}}
-\pagestyle{plain}
-
-% --------------------------------------------------------------------------
-% --- Cover Page ---
-% --------------------------------------------------------------------------
-\newcommand{\coverpage}[1]{%
-\thispagestyle{empty}
-\setlength\unitlength{1cm}
-\begin{picture}(0,0)(3.27,26.75)
-\put(0.58,0.70){\includegraphics[width=20.9cm]{frama-c-cover.pdf}}
-\put(2.0,20.5){\makebox[8cm][l]{\fontfamily{phv}\fontseries{m}\fontsize{24}{2}\selectfont #1}}
-\end{picture}
-}
-
-% --------------------------------------------------------------------------
-% --- Title Page ---
-% --------------------------------------------------------------------------
-\renewenvironment{titlepage}%
-{\cleardoublepagewith{empty}\thispagestyle{empty}\begin{center}}%
-{\end{center}}
-\renewcommand{\title}[2]{
-\vspace{20mm}
-{\Huge\bfseries #1}
-
-\bigskip
-
-{\LARGE #2}
-\vspace{20mm}
-}
-\renewcommand{\author}[1]{
-\vspace{20mm}
-
-{#1}
-
-\medskip
-}
-% --------------------------------------------------------------------------
-% --- Sectionning ---
-% --------------------------------------------------------------------------
-\titleformat{\chapter}[display]{\Huge\raggedleft}%
-{\huge\chaptertitlename\,\thechapter}{0.5em}{}
-\titleformat{\section}[hang]{\Large\bfseries}{\thesection}{1em}{}%
-[\vspace{-14pt}\rule{\textwidth}{0.1pt}\vspace{-8pt}]
-\titleformat{\subsubsection}[hang]{\bfseries}{}{}{}%
-[\vspace{-8pt}]
-
-% --------------------------------------------------------------------------
-% --- Main Text Style ---
-% --------------------------------------------------------------------------
-%\raggedright
-\setlength\parindent{0pt}
-\setlength\parskip{1ex plus 0.3ex minus 0.2ex}
-\newenvironment{warning}[1][Warning:]{\small\paragraph{#1}\itshape}{\vspace{\parskip}}
-\def\FramaC{\textsf{Frama-C}\xspace}
-% --------------------------------------------------------------------------
-% --- Listings ---
-% --------------------------------------------------------------------------
-\RequirePackage{listings}
-
-\lstdefinelanguage{ACSL}{%
- morekeywords={allocates,assert,assigns,assumes,axiom,axiomatic,behavior,behaviors,
- boolean,breaks,complete,continues,data,decreases,disjoint,ensures,
- exit_behavior,frees,ghost,global,inductive,integer,invariant,lemma,logic,loop,
- model,predicate,reads,real,requires,returns,sizeof,strong,struct,terminates,type,
- union,variant},
- keywordsprefix={\\},
- alsoletter={\\},
- morecomment=[l]{//}
-}
-
-\lstloadlanguages{[ANSI]C,[Objective]Caml,csh,ACSL}
-\definecolor{lstbg}{gray}{0.98}
-\definecolor{lstfg}{gray}{0.10}
-\definecolor{lstrule}{gray}{0.6}
-\definecolor{lstnum}{gray}{0.4}
-\definecolor{lsttxt}{rgb}{0.3,0.2,0.6}
-\definecolor{lstmodule}{rgb}{0.3,0.6,0.2}%{0.6,0.6,0.2}
-\definecolor{lstspecial}{rgb}{0.2,0.6,0.0}
-\definecolor{lstfile}{gray}{0.85}
-\newcommand{\lstbrk}{\mbox{$\color{blue}\scriptstyle\cdots$}}
-\def\lp@basic{\ifmmode\normalfont\mathtt\mdseries\small\else\normalfont\ttfamily\mdseries\small\fi}
-\def\lp@inline{\ifmmode\normalfont\mathtt\scriptstyle\else\normalfont\ttfamily\mdseries\small\fi}
-\def\lp@keyword{}
-\def\lp@special{\color{lstfg}}
-\def\lp@comment{\normalfont\ttfamily\mdseries}
-\def\lp@string{\color{lstfg}} \def\lp@ident{}
-\def\lp@number{\rmfamily\tiny\color{lstnum}}
-\lstdefinestyle{frama-c-style}{%
- columns=flexible,%
- basicstyle=\lp@inline,%
- identifierstyle=\lp@ident,%
- commentstyle=\lp@comment,%
- keywordstyle={\ifmmode\mathsf\else\sffamily\fi},%
- keywordstyle=[2]\lp@special,%
- stringstyle=\lp@string,%
- emphstyle=\lp@ident\underbar,%
- showstringspaces=false,%
- mathescape=true,%
- numberstyle=\lp@number,%
- xleftmargin=6ex,xrightmargin=2ex,%
- framexleftmargin=1ex,%
- frame=l,%
- framerule=1pt,%
- rulecolor=\color{lstrule},%
- backgroundcolor=\color{lstbg},%
- moredelim={*[s]{/*@}{*/}},%
- moredelim={*[l]{//@}},%
- morecomment={[il]{//NOPP-LINE}},% invisible comment until end of line
- morecomment={[is]{//NOPP-BEGIN}{NOPP-END\^^M}},% no space after NOPP-END
- mathescape=true,
- escapechar=`
-% breaklines is broken when using a inline and background
-% breaklines,prebreak={\lstbrk},postbreak={\lstbrk},breakindent=5ex %
-}
-
-\lstdefinestyle{c}%
-{language={[ANSI]C},alsolanguage=ACSL,style=frama-c-style}
-\lstdefinestyle{c-basic}%
-{language={[ANSI]C},alsolanguage=ACSL,style=frama-c-style,basicstyle=\lp@basic}
-
-
-% --- C/ACSL Stuff ---------------------------------------------------------
-% Make 'c' the default style
-\lstset{style=c}
-
-\newcommand{\listinginput}[3][1]%
-{\lstinputlisting[style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2]{#3}}
-
-\newcommand{\listinginputcaption}[4][1]%
-{\lstinputlisting[style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2,title=#3]{#4}}
-
-\lstnewenvironment{listing}[2][1]%
-{\lstset{style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2}}{}
-
-\lstnewenvironment{listing-nonumber}%
-{\lstset{style=c,numbers=none,basicstyle=\lp@basic}}{}
-
-% --- Verbatim Stuff -------------------------------------------------------
-\lstdefinelanguage{Shell}[]{csh}%
-{escapechar=@
- identifierstyle=\lp@basic,
- mathescape=false,
- backgroundcolor=,
- literate={\\\$}{\$}1
-}
-
-\lstnewenvironment{shell}[1][]
-{\lstset{language=Shell,basicstyle=\lp@basic,#1}}
-{}
-
-% ---- Stdout Stuff --------------------------------------------------------
-\lstdefinelanguage{Logs}[]{csh}%
-{identifierstyle=\lp@basic,backgroundcolor=}
-\lstnewenvironment{logs}[1][]{\lstset{language=Logs,basicstyle=\lp@basic,#1}}{}
-\newcommand{\logsinput}[1]%
-{\lstinputlisting[language=Logs,basicstyle=\lp@basic]{#1}}
-
-% --------------------------------------------------------------------------
-% --- Developer Code Stuff ---
-% --------------------------------------------------------------------------
-
-\newcommand{\listingname}[1]{\colorbox{lstfile}{\footnotesize\sffamily File \bfseries #1}\vspace{-4pt}}
-
-% --- Style ----------------------------------------------------------------
-\lstdefinestyle{framac-code-style}{%
-basicstyle=\lp@inline,%
-numberstyle=\lp@number,%
-keywordstyle=[1]\sffamily\color{lstmodule},%
-keywordstyle=[2]\sffamily\color{lstspecial},%
-keywordstyle=[3]\sffamily\bfseries,%
-identifierstyle=\rmfamily,%
-stringstyle=\ttfamily\color{lstfg},%
-commentstyle=\rmfamily\bfseries\color{lsttxt},%
-}
-\lstdefinestyle{framac-shell-style}{%
-mathescape=false,%
-basicstyle=\lp@basic,%
-numberstyle=\lp@number,%
-keywordstyle=\sffamily\bfseries,%
-keywordstyle=[1]\sffamily\color{lstmodule},%
-keywordstyle=[2]\sffamily\color{lstspecial},%
-keywordstyle=[3]\sffamily\bfseries,%
-identifierstyle=\ttfamily,%
-stringstyle=\ttfamily\color{lstfg},%
-commentstyle=\rmfamily\bfseries\color{lsttxt},%
-literate={\\\$}{\$}1%
-{€}{\textbackslash}1%
-,%
-}
-% --- Configure ------------------------------------------------------------
-\lstdefinelanguage{Configure}[]{csh}{%
-style=framac-shell-style,%
-morekeywords={fi},%
-}
-\lstnewenvironment{configurecode}[1][]%
-{\lstset{language=Configure,#1}}{}
-\newcommand{\configureinput}[1]{\lstinputlisting[language=Configure]{#1}}
-% --- Makefile ------------------------------------------------------------
-\lstdefinelanguage{Makefile}[]{make}{%
-style=framac-shell-style,%
-morekeywords={include},%
-}
-\lstnewenvironment{makefilecode}[1][]%
-{\lstset{language=Makefile,#1}}{}
-\newcommand{\makefileinput}[1]{\lstinputlisting[language=Makefile]{#1}}
-% --- C- for Developer ----------------------------------------------------
-\lstdefinestyle{framac-code}%
- {language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic}
-\lstnewenvironment{ccode}[1][]%
-{\lstset{language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic,#1}}{}
-\newcommand{\cinput}[1]%
-{\lstinputlisting[language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic]{#1}}
-\newcommand{\cinline}[1]%
-{\lstinline[style=framac-code]{#1}}
-% --- Ocaml ----------------------------------------------------------------
-\lstdefinelanguage{Ocaml}[Objective]{Caml}{%
-style=framac-code-style,%
-deletekeywords={when,module,struct,sig,begin,end},%
-morekeywords=[2]{failwith,raise,when},%
-morekeywords=[3]{module,struct,sig,begin,end},%
-literate=%
-{~}{${\scriptstyle\thicksim}$}1%
-{<}{$<$ }1%
-{>}{$>$ }1%
-{->}{$\rightarrow$ }1%
-{<-}{$\leftarrow$ }1%
-{:=}{$\leftarrow$ }1%
-{<=}{$\leq$ }1%
-{>=}{$\geq$ }1%
-{==}{$\equiv$ }1%
-{!=}{$\not\equiv$ }1%
-{<>}{$\neq$ }1%
-{'a}{$\alpha$ }1%
-{'b}{$\beta$ }1%
-{'c}{$\gamma$ }1%
-{µ}{`{}}1%
-{€}{\textbackslash}1%
-}
-
-\lstdefinestyle{ocaml-basic}%
-{language=Ocaml,basicstyle=\lp@basic}
-\newcommand{\ocamlinput}[2][]{\lstinputlisting[style=ocaml-basic,#1]{#2}}
-\lstnewenvironment{ocamlcode}[1][]{\lstset{style=ocaml-basic,#1}}{}
-% --------------------------------------------------------------------------
-\lstdefinelanguage{Why}{%
- morekeywords={
- type, logic, axiom, predicate, goal,
- forall, let, in,
- },
- morecomment=[s]{(*}{*)},
- alsoletter={_},
- literate=%
- {->}{$\Rightarrow$}1%
- {forall}{$\forall$}1%
- {not}{$\neg$}1%
- {<>}{$\neq$}1%
- {...}{$\dots$}1%
- %{_}{\_}1%
- %{_}{{\rule[0pt]{1ex}{.2pt}}}1%
- }
-
-\lstdefinestyle{why-style}{%
-language=Why,%
-style=framac-code-style,%
-basicstyle=\lp@inline,%
-}
-
-\lstnewenvironment{whycode}[1][]{\lstset{style=why-style,#1}}{}
-\newcommand{\whyinput}[1]%
-{\lstinputlisting[style=why-style,basicstyle=\lp@basic]{#1}}
-\newcommand{\whyinline}[1]%
-{\lstinline[style=why-style]{#1}}
-
-% --------------------------------------------------------------------------
-% --- End. ---
-% --------------------------------------------------------------------------
diff --git a/src/plugins/wp/doc/manual/wp.tex b/src/plugins/wp/doc/manual/wp.tex
index 7179925a8b949236ae4618e79657d377f124755d..e1c630967ebe1f8af4cc95be8f4fb84a0ac3d320 100644
--- a/src/plugins/wp/doc/manual/wp.tex
+++ b/src/plugins/wp/doc/manual/wp.tex
@@ -22,12 +22,11 @@
{\tt Frama-C \FCVERSION}
\author{Patrick Baudin, François Bobot, Loïc Correnson, Zaynah Dargaye}
\begin{center}
-CEA LIST, Software Safety Laboratory \\
-May, 2016
+CEA LIST, Software Safety Laboratory
\end{center}
\vfill
\begin{flushleft}
- \textcopyright 2010-2016 CEA LIST
+ \textcopyright 2010-{\the\year} CEA LIST
This work has been partially supported by the 'U3CAT' ANR project.
\end{flushleft}