frama-c / frama-c-snapshot Goto Github PK

ANSI/ISO C Specification Language

opam init
opam install depext
opam depext frama-c
opam install frama-c

frama-c file.c -<plugin> [options]
frama-c-gui file.c

frama-c -plugins

frama-c -kernel-help

frama-c *.c *.h -cpp-extra-args="-D<define> -I<include>" -save parsed.sav

frama-c -load parsed.sav -<plugin> [options]
frama-c-gui -load parsed.sav -<plugin> [options]

/*@
  requires 0 < n;
  assigns  \nothing;
*/
int loop(int n)
{
   int a = 0;
   /*@
     loop invariant 0 <= i <= n;
     loop invariant a == i;
     loop assigns i, a;

     // note these two lines
     loop variant n-i;
     //loop invariant n-i;
   */
   for(int i = 0; i < n; ++i) {
      a += 1;
   }

  return a;
}

/*@ axiomatic maps { type model_digit = octet | sextet; 
                     logic integer foo(model_digit i);
                   }
*/
int foo() {
//@assert \forall int i;  i == foo(octet);
  return 0;
}
$ frama-c -wp -wp-prover z3-ce simple.c
[kernel] Parsing simple.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] WPOUT/typed/A_maps.why:13: User Error: why3 syntax error
[wp] [z3-ce] Goal typed_foo_assert : Failed
  why3 syntax error
[wp] Proved goals:    0 / 1
  Why3 (z3-ce):    0  (failed: 1)
[wp] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Plug-in wp aborted: invalid user input.
(* ---------------------------------------------------------- *)
(* --- Axiomatic 'maps'                                   --- *)
(* ---------------------------------------------------------- *)
theory A_maps

use bool.Bool
use int.Int
use int.ComputerDivision
use real.RealInfix
use Qed.Qed
use int.Abs as IAbs
use map.Map
type a_model_digit | c_octet | c_sextet

function l_foo a_model_digit : int

end

type a_model_digit | c_octet | c_sextet

checking for frama-c-gui... yes
checking for Makefile.config.in... yes
frama_clang... yes
checking for g++... g++
checking whether the C++ compiler works... yes
checking for C++ compiler default output file name... a.out
checking for suffix of executables... 
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether we are using the GNU C++ compiler... yes
checking whether g++ accepts -g... yes
checking for camlp4o... yes
checking for clang... clang
checking for clang++... clang++
checking for llvm-config... llvm-config
checking for /usr/lib/llvm-4.0/include/clang... no
configure: WARNING: frama_clang disabled because clang dev headers not found.
configure: frama_clang: no
configure: creating ./config.status
config.status: creating ./Makefile.config

lenovo@vishrutidesai:~$ opam install frama-c.20181101
The following actions will be performed:
  - install frama-c 20181101
       Yojson enables kernel option -json-compilation-database
       Why3 can be used by the WP plug-in for running additional automatic solvers
       Coq can be used with the WP plug-in for proving interactively proof obligations

=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[frama-c] Archive in cache

=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[ERROR] The compilation of frama-c failed at "make -j4".
Processing  1/1: [frama-c: rm]
#=== ERROR while installing frama-c.20181101 ==================================#
# opam-version 1.2.2
# os           linux
# command      make -j4
# path         /home/lenovo/.opam/4.02.3/build/frama-c.20181101
# compiler     4.02.3
# exit-code    2
# env-file     /home/lenovo/.opam/4.02.3/build/frama-c.20181101/frama-c-67682-58c514.env
# stdout-file  /home/lenovo/.opam/4.02.3/build/frama-c.20181101/frama-c-67682-58c514.out
# stderr-file  /home/lenovo/.opam/4.02.3/build/frama-c.20181101/frama-c-67682-58c514.err
### stdout ###
# [...]
# Generating   src/plugins/wp/tests/ptests_config
# Ocamlc       src/plugins/aorai/bool3.cmo
# Ocamlc       src/libraries/datatype/structural_descr.cmi
# Ocamlc       src/kernel_services/plugin_entry_points/log.cmi
# Ocamlc       src/libraries/stdlib/integer.cmi
# Ocamlc       src/plugins/aorai/ltl_output.cmi
# Ocamlc       src/kernel_services/abstract_interp/float_sig.cmi
# Ocamlopt     src/libraries/datatype/structural_descr.cmx
# Ocamlopt     src/libraries/stdlib/transitioning.cmx
# Ocamlopt     src/libraries/stdlib/FCBuffer.cmx
### stderr ###
# 4 shift/reduce conflicts.
# 7 shift/reduce conflicts.
# File "src/libraries/stdlib/transitioning.ml", line 104, characters 15-24:
# Error: Unbound value Z.numbits
# Hint: Did you mean to_bits or of_bits?
# make: *** [share/Makefile.generic:89: src/libraries/stdlib/transitioning.cmx] Error 2
# make: *** Waiting for unfinished jobs....

=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
The following actions failed
  - install frama-c 20181101
No changes have been performed

/*
From https://raw.githubusercontent.com/Frama-C/Frama-C-snapshot/master/src/kernel_internals/parsing/cparser.mly
*/

interpret ::=  file
file ::=  globals EOF
globals ::=  /* empty */ | global globals | ghost_glob_begin ghost_globals globals | SEMICOLON globals
ghost_glob_begin ::=  LGHOST
ghost_globals ::=  declaration ghost_globals | function_def ghost_globals | RGHOST
global ::=  DECL | CUSTOM_ANNOT | declaration | function_def | EXTERN string_constant declaration | EXTERN string_constant LBRACE globals RBRACE | ASM LPAREN string_constant RPAREN SEMICOLON | pragma | IDENT LPAREN old_parameter_list_ne RPAREN old_pardef_list SEMICOLON | IDENT LPAREN RPAREN SEMICOLON
id_or_typename_as_id ::=  IDENT | NAMED_TYPE
id_or_typename ::=  id_or_typename_as_id
maybecomma ::=  /* empty */ | COMMA
primary_expression ::=  IDENT | constant | paren_comma_expression | LPAREN block RPAREN
postfix_expression ::=  primary_expression | postfix_expression bracket_comma_expression | postfix_expression LPAREN arguments RPAREN ghost_arguments_opt | BUILTIN_VA_ARG LPAREN expression COMMA type_name RPAREN | BUILTIN_TYPES_COMPAT LPAREN type_name COMMA type_name RPAREN | BUILTIN_OFFSETOF LPAREN type_name COMMA offsetof_member_designator RPAREN | postfix_expression DOT id_or_typename | postfix_expression ARROW id_or_typename | postfix_expression PLUS_PLUS | postfix_expression MINUS_MINUS | LPAREN type_name RPAREN LBRACE initializer_list_opt RBRACE
offsetof_member_designator ::=  id_or_typename | offsetof_member_designator DOT IDENT | offsetof_member_designator bracket_comma_expression
unary_expression ::=  postfix_expression | PLUS_PLUS unary_expression | MINUS_MINUS unary_expression | SIZEOF unary_expression | SIZEOF LPAREN type_name RPAREN | ALIGNOF unary_expression | ALIGNOF LPAREN type_name RPAREN | PLUS cast_expression | MINUS cast_expression | STAR cast_expression | AND cast_expression | EXCLAM cast_expression | TILDE cast_expression | AND_AND id_or_typename_as_id
cast_expression ::=  unary_expression | LPAREN type_name RPAREN cast_expression
multiplicative_expression ::=  cast_expression | multiplicative_expression STAR cast_expression | multiplicative_expression SLASH cast_expression | multiplicative_expression PERCENT cast_expression
additive_expression ::=  multiplicative_expression | additive_expression PLUS multiplicative_expression | additive_expression MINUS multiplicative_expression
shift_expression ::=  additive_expression | shift_expression INF_INF additive_expression | shift_expression SUP_SUP additive_expression
relational_expression ::=  shift_expression | relational_expression INF shift_expression | relational_expression SUP shift_expression | relational_expression INF_EQ shift_expression | relational_expression SUP_EQ shift_expression
equality_expression ::=  relational_expression | equality_expression EQ_EQ relational_expression | equality_expression EXCLAM_EQ relational_expression
bitwise_and_expression ::=  equality_expression | bitwise_and_expression AND equality_expression
bitwise_xor_expression ::=  bitwise_and_expression | bitwise_xor_expression CIRC bitwise_and_expression
bitwise_or_expression ::=  bitwise_xor_expression | bitwise_or_expression PIPE bitwise_xor_expression
logical_and_expression ::=  bitwise_or_expression | logical_and_expression AND_AND bitwise_or_expression
logical_or_expression ::=  logical_and_expression | logical_or_expression PIPE_PIPE logical_and_expression
conditional_expression ::=  logical_or_expression | logical_or_expression QUEST opt_expression COLON conditional_expression
assignment_expression ::=  conditional_expression | cast_expression EQ assignment_expression | cast_expression PLUS_EQ assignment_expression | cast_expression MINUS_EQ assignment_expression | cast_expression STAR_EQ assignment_expression | cast_expression SLASH_EQ assignment_expression | cast_expression PERCENT_EQ assignment_expression | cast_expression AND_EQ assignment_expression | cast_expression PIPE_EQ assignment_expression | cast_expression CIRC_EQ assignment_expression | cast_expression INF_INF_EQ assignment_expression | cast_expression SUP_SUP_EQ assignment_expression
expression ::=  assignment_expression
constant ::=  CST_INT | CST_FLOAT | CST_CHAR | CST_WCHAR | string_constant | wstring_list
string_constant ::=  string_list
string_list ::=  one_string | string_list one_string
wstring_list ::=  CST_WSTRING | wstring_list one_string | wstring_list CST_WSTRING | string_list CST_WSTRING
one_string ::=  CST_STRING | FUNCTION__ | PRETTY_FUNCTION__
init_expression ::=  expression | LBRACE initializer_list_opt RBRACE
initializer_list ::=  initializer_single | initializer_single COMMA initializer_list_opt
initializer_list_opt ::=  /* empty */ | initializer_list
initializer_single ::=  init_designators eq_opt init_expression | gcc_init_designators init_expression | init_expression
eq_opt ::=   /* empty */ | EQ
init_designators ::=  DOT id_or_typename init_designators_opt | LBRACKET expression RBRACKET init_designators_opt | LBRACKET expression ELLIPSIS expression RBRACKET
init_designators_opt ::=  /* empty */ | init_designators
gcc_init_designators ::=  id_or_typename COLON
ghost_arguments_opt ::=  /* empty */ | ghost_arguments
ghost_arguments ::=  LGHOST LPAREN arguments RPAREN RGHOST
arguments ::=  /* empty */ | comma_expression
opt_expression ::=  /* empty */ | comma_expression
comma_expression ::=  expression | expression COMMA comma_expression
comma_expression_opt ::=  /* empty */ | comma_expression
paren_comma_expression ::=  LPAREN comma_expression RPAREN
bracket_comma_expression ::=  LBRACKET comma_expression RBRACKET
block ::=  block_begin local_labels block_attrs block_element_list RBRACE
block_begin ::=  LBRACE
block_attrs ::=  /* empty */ | BLOCKATTRIBUTE paren_attr_list_ne
block_element_list ::=  annot_list_opt | annot_list_opt declaration block_element_list | annot_list_opt statement block_element_list | annot_list_opt pragma block_element_list | annot_list_opt id_or_typename_as_id COLON
annot_list_opt ::=  /* empty */ | annot_list
annot_list ::=  CODE_ANNOT annot_list_opt | LGHOST block_element_list RGHOST annot_list_opt
local_labels ::=  /* empty */ | LABEL__ local_label_names SEMICOLON local_labels
local_label_names ::=  id_or_typename_as_id | id_or_typename_as_id COMMA local_label_names
annotated_statement ::=  statement | annot_list statement
statement ::=  SEMICOLON | SPEC annotated_statement | comma_expression SEMICOLON | block | IF paren_comma_expression annotated_statement | IF paren_comma_expression annotated_statement ELSE annotated_statement | SWITCH paren_comma_expression annotated_statement | opt_loop_annotations WHILE paren_comma_expression annotated_statement | opt_loop_annotations DO annotated_statement WHILE paren_comma_expression SEMICOLON | opt_loop_annotations FOR LPAREN for_clause opt_expression SEMICOLON opt_expression RPAREN annotated_statement | id_or_typename_as_id COLON attribute_nocv_list annotated_statement | CASE expression COLON annotated_statement | CASE expression ELLIPSIS expression COLON annotated_statement | DEFAULT COLON annotated_statement | RETURN SEMICOLON | RETURN comma_expression SEMICOLON | BREAK SEMICOLON | CONTINUE SEMICOLON | GOTO id_or_typename_as_id SEMICOLON | GOTO STAR comma_expression SEMICOLON | ASM GOTO asmattr LPAREN asmtemplate asmoutputs RPAREN SEMICOLON | ASM asmattr LPAREN asmtemplate asmoutputs RPAREN SEMICOLON | MSASM | TRY block EXCEPT paren_comma_expression block | TRY block FINALLY block
opt_loop_annotations ::=  /* empty */ | loop_annotations
loop_annotations ::=  loop_annotation
loop_annotation ::=  LOOP_ANNOT
for_clause ::=  opt_expression SEMICOLON | declaration
ghost_parameter_opt ::=  /* empty */ | ghost_parameter
ghost_parameter ::=  LGHOST parameter_list_startscope rest_par_list RPAREN RGHOST
declaration ::=  decl_spec_list init_declarator_list SEMICOLON | decl_spec_list SEMICOLON | SPEC decl_spec_list init_declarator_list SEMICOLON | SPEC decl_spec_list SEMICOLON
init_declarator_list ::=  init_declarator | init_declarator COMMA init_declarator_attr_list
init_declarator_attr_list ::=  init_declarator_attr | init_declarator_attr COMMA init_declarator_attr_list
init_declarator_attr ::=  attribute_nocv_list init_declarator
init_declarator ::=  declarator | declarator EQ init_expression
decl_spec_wo_type ::=  TYPEDEF | EXTERN | STATIC | AUTO | REGISTER | INLINE | cvspec | attribute_nocv
decl_spec_list ::=  decl_spec_wo_type decl_spec_list_opt | type_spec decl_spec_list_opt_no_named
decl_spec_list_no_named ::=  decl_spec_wo_type decl_spec_list_opt_no_named | type_spec decl_spec_list_opt_no_named
decl_spec_list_opt ::=  /* empty */ | decl_spec_list
decl_spec_list_opt_no_named ::=  /* empty */ | decl_spec_list_no_named
type_spec ::=  VOID | CHAR | BOOL | SHORT | INT | LONG | INT64 | FLOAT | DOUBLE | SIGNED | UNSIGNED | STRUCT id_or_typename | STRUCT just_attributes id_or_typename | STRUCT id_or_typename LBRACE struct_decl_list RBRACE | STRUCT LBRACE struct_decl_list RBRACE | STRUCT just_attributes id_or_typename LBRACE struct_decl_list RBRACE | STRUCT just_attributes LBRACE struct_decl_list RBRACE | UNION id_or_typename | UNION id_or_typename LBRACE struct_decl_list RBRACE | UNION LBRACE struct_decl_list RBRACE | UNION just_attributes id_or_typename LBRACE struct_decl_list RBRACE | UNION just_attributes LBRACE struct_decl_list RBRACE | ENUM id_or_typename | ENUM id_or_typename LBRACE enum_list maybecomma RBRACE | ENUM LBRACE enum_list maybecomma RBRACE | ENUM just_attributes id_or_typename LBRACE enum_list maybecomma RBRACE | ENUM just_attributes LBRACE enum_list maybecomma RBRACE | NAMED_TYPE | TYPEOF LPAREN expression RPAREN | TYPEOF LPAREN type_name RPAREN
struct_decl_list ::=  /* empty */ | decl_spec_list SEMICOLON struct_decl_list | SEMICOLON struct_decl_list | decl_spec_list field_decl_list SEMICOLON struct_decl_list | pragma struct_decl_list
field_decl_list ::=  field_decl | field_decl COMMA field_decl_list
field_decl ::=  declarator | declarator COLON expression attributes | COLON expression
enum_list ::=  enumerator | enum_list COMMA enumerator
enumerator ::=  IDENT | IDENT EQ expression
declarator ::=  pointer_opt direct_decl attributes_with_asm
attributes_or_static ::=  attributes comma_expression_opt | attribute attributes STATIC comma_expression | STATIC attributes comma_expression
direct_decl ::=  id_or_typename | LPAREN attributes declarator RPAREN | direct_decl LBRACKET attributes_or_static RBRACKET | direct_decl LPAREN RPAREN ghost_parameter_opt | direct_decl parameter_list_startscope rest_par_list RPAREN ghost_parameter_opt
parameter_list_startscope ::=  LPAREN
rest_par_list ::=  parameter_decl rest_par_list1
rest_par_list1 ::=  /* empty */ | COMMA ELLIPSIS | COMMA parameter_decl rest_par_list1
parameter_decl ::=  decl_spec_list declarator | decl_spec_list abstract_decl | decl_spec_list | LPAREN parameter_decl RPAREN
old_proto_decl ::=  pointer_opt direct_old_proto_decl
direct_old_proto_decl ::=  direct_decl LPAREN old_parameter_list_ne RPAREN old_pardef_list
old_parameter_list_ne ::=  IDENT | IDENT COMMA old_parameter_list_ne
old_pardef_list ::=  /* empty */ | decl_spec_list old_pardef SEMICOLON ELLIPSIS | decl_spec_list old_pardef SEMICOLON old_pardef_list
old_pardef ::=  declarator | declarator COMMA old_pardef
pointer ::=  STAR attributes pointer_opt
pointer_opt ::=  /* empty */ | pointer
type_name ::=  decl_spec_list abstract_decl | decl_spec_list
abstract_decl ::=  pointer_opt abs_direct_decl attributes | pointer
abs_direct_decl ::=  LPAREN attributes abstract_decl RPAREN | abs_direct_decl_opt LBRACKET comma_expression_opt RBRACKET | abs_direct_decl parameter_list_startscope rest_par_list RPAREN | abs_direct_decl LPAREN RPAREN
abs_direct_decl_opt ::=   /* empty */ | abs_direct_decl
function_def ::=  SPEC function_def_start block | function_def_start block
function_def_start ::=  decl_spec_list declarator | decl_spec_list old_proto_decl | IDENT parameter_list_startscope rest_par_list RPAREN ghost_parameter_opt | IDENT LPAREN old_parameter_list_ne RPAREN old_pardef_list | IDENT LPAREN RPAREN ghost_parameter_opt
cvspec ::=  CONST | VOLATILE | RESTRICT | ATTRIBUTE_ANNOT
attributes ::=  /* empty */ | attribute attributes
attributes_with_asm ::=  /* empty */ | attribute attributes_with_asm | ASM LPAREN string_constant RPAREN attributes
attribute_nocv ::=  ATTRIBUTE LPAREN paren_attr_list RPAREN | DECLSPEC paren_attr_list_ne | MSATTR | THREAD
attribute_nocv_list ::=  /* empty */ | attribute_nocv attribute_nocv_list
attribute ::=  attribute_nocv | CONST | RESTRICT | VOLATILE | ATTRIBUTE_ANNOT
just_attribute ::=  ATTRIBUTE LPAREN paren_attr_list RPAREN | DECLSPEC paren_attr_list_ne
just_attributes ::=  just_attribute | just_attribute just_attributes
pragma ::=  PRAGMA PRAGMA_EOL | PRAGMA attr PRAGMA_EOL | PRAGMA attr SEMICOLON PRAGMA_EOL | PRAGMA_LINE
var_attr ::=  IDENT | NAMED_TYPE | DEFAULT COLON CST_INT | CONST | VOLATILE | CST_INT COLON CST_INT
basic_attr ::=  CST_INT | CST_FLOAT | var_attr
basic_attr_list_ne ::=  basic_attr | basic_attr basic_attr_list_ne
parameter_attr_list_ne ::=  basic_attr_list_ne | basic_attr_list_ne string_constant | basic_attr_list_ne string_constant parameter_attr_list_ne
param_attr_list_ne ::=  parameter_attr_list_ne | string_constant
primary_attr ::=  basic_attr | LPAREN attr RPAREN | string_constant
postfix_attr ::=  primary_attr | id_or_typename_as_id paren_attr_list_ne | id_or_typename_as_id LPAREN RPAREN | basic_attr param_attr_list_ne | postfix_attr ARROW id_or_typename | postfix_attr DOT id_or_typename | postfix_attr LBRACKET attr RBRACKET
unary_attr ::=  postfix_attr | SIZEOF unary_expression | SIZEOF LPAREN type_name RPAREN | ALIGNOF unary_expression | ALIGNOF LPAREN type_name RPAREN | PLUS cast_attr | MINUS cast_attr | STAR cast_attr | AND cast_attr | EXCLAM cast_attr | TILDE cast_attr
cast_attr ::=  unary_attr
multiplicative_attr ::=  cast_attr | multiplicative_attr STAR cast_attr | multiplicative_attr SLASH cast_attr | multiplicative_attr PERCENT cast_attr
additive_attr ::=  multiplicative_attr | additive_attr PLUS multiplicative_attr | additive_attr MINUS multiplicative_attr
shift_attr ::=  additive_attr | shift_attr INF_INF additive_attr | shift_attr SUP_SUP additive_attr
relational_attr ::=  shift_attr | relational_attr INF shift_attr | relational_attr SUP shift_attr | relational_attr INF_EQ shift_attr | relational_attr SUP_EQ shift_attr
equality_attr ::=  relational_attr | equality_attr EQ_EQ relational_attr | equality_attr EXCLAM_EQ relational_attr
bitwise_and_attr ::=  equality_attr | bitwise_and_attr AND equality_attr
bitwise_xor_attr ::=  bitwise_and_attr | bitwise_xor_attr CIRC bitwise_and_attr
bitwise_or_attr ::=  bitwise_xor_attr | bitwise_or_attr PIPE bitwise_xor_attr
logical_and_attr ::=  bitwise_or_attr | logical_and_attr AND_AND bitwise_or_attr
logical_or_attr ::=  logical_and_attr | logical_or_attr PIPE_PIPE logical_and_attr
conditional_attr ::=  logical_or_attr | logical_or_attr QUEST attr_test conditional_attr COLON2 conditional_attr
assign_attr ::=  conditional_attr | conditional_attr EQ conditional_attr
attr_test ::=  /* empty */
attr ::=  assign_attr
attr_list_ne ::=  attr | attr COMMA attr_list_ne
attr_list ::=  /* empty */ | attr_list_ne
paren_attr_list_ne ::=  LPAREN attr_list_ne RPAREN
paren_attr_list ::=  LPAREN attr_list RPAREN
asmattr ::=  /* empty */ | VOLATILE asmattr | CONST asmattr
asmtemplate ::=  one_string | one_string asmtemplate
asmoutputs ::=  /* empty */ | COLON asmoperands asminputs
asmoperands ::=  /* empty */ | asmoperandsne
asmoperandsne ::=  asmoperand | asmoperandsne COMMA asmoperand
asmoperand ::=  asmopname string_constant LPAREN expression RPAREN
asminputs ::=  /* empty */ | COLON asmoperands asmclobber
asmopname ::=  /* empty */ | LBRACKET IDENT RBRACKET
asmclobber ::=  /* empty */ | COLON asmlabels | COLON asmcloberlst_ne asmlabels
asmcloberlst_ne ::=  string_constant | string_constant COMMA asmcloberlst_ne
asmlabels ::=  /* empty */ | COLON local_label_names

// Tokens

AUTO ::= "auto"
CONST ::= "const"
CONST ::= "__const"
CONST ::= "__const__"
STATIC ::= "static"
EXTERN ::= "extern"
LONG ::= "long"
SHORT ::= "short"
REGISTER ::= "register"
SIGNED ::= "signed"
SIGNED ::= "__signed"
UNSIGNED ::= "unsigned"
VOLATILE ::= "volatile"
VOLATILE ::= "__volatile"
/* WW: see /usr/include/sys/cdefs.h for why __signed and __volatile * are accepted GCC-isms */
CHAR ::= "char"
BOOL ::= "_Bool"
INT ::= "int"
FLOAT ::= "float"
DOUBLE ::= "double"
VOID ::= "void"
ENUM ::= "enum"
STRUCT ::= "struct"
TYPEDEF ::= "typedef"
UNION ::= "union"
BREAK ::= "break"
CONTINUE ::= "continue"
GOTO ::= "goto"
RETURN ::= "return"
SWITCH ::= "switch"
CASE ::= "case"
DEFAULT ::= "default"
WHILE ::= "while"
DO ::= "do"
FOR ::= "for"
IF ::= "if"
ELSE ::= "else"
/*** Implementation specific keywords ***/
SIGNED ::= "__signed__"
INLINE ::= "__inline__" | "inline" | "__inline" | "_inline" | __forceinline /* !! we turn forceinline
			 * into inline */
ATTRIBUTE ::= "__attribute__"
ATTRIBUTE ::= "__attribute"
BLOCKATTRIBUTE ::= "__blockattribute__" | "__blockattribute"
ASM ::= "__asm__"
ASM ::= "asm"
TYPEOF ::= "__typeof__"
TYPEOF ::= "__typeof"
TYPEOF ::= "typeof"
ALIGNOF ::= "__alignof"
ALIGNOF ::= "__alignof__"
VOLATILE ::= "__volatile__"
VOLATILE ::= "__volatile"
FUNCTION__ ::= "__FUNCTION__"
FUNCTION__ ::= "__func__" /* ISO 6.4.2.2 */
PRETTY_FUNCTION__ ::= "__PRETTY_FUNCTION__"
LABEL__ ::= "__label__"
/*** weimer: GCC arcana ***/
RESTRICT ::= "__restrict"
RESTRICT ::= "restrict"
/*      ("__extension__", EXTENSION); */
/**** MS VC ***/
INT64 ::= "__int64"
INT ::= "__int32"
/*
("_cdecl",  fun _ -> MSATTR ("_cdecl", currentLoc ()));
("__cdecl", fun _ -> MSATTR ("__cdecl", currentLoc ()));
("_stdcall", fun _ -> MSATTR ("_stdcall", currentLoc ()));
("__stdcall", fun _ -> MSATTR ("__stdcall", currentLoc ()));
("_fastcall", fun _ -> MSATTR ("_fastcall", currentLoc ()));
("__fastcall", fun _ -> MSATTR ("__fastcall", currentLoc ()));
("__w64", fun _ -> MSATTR("__w64", currentLoc ()));
*/
DECLSPEC ::= "__declspec"
TRY ::= "__try"
EXCEPT ::= "__except"
FINALLY ::= "__finally"
/* weimer: some files produced by 'GCC -E' expect this type to be * defined */
NAMED_TYPE ::= "__builtin_va_list"
BUILTIN_VA_ARG ::= "__builtin_va_arg"
BUILTIN_TYPES_COMPAT ::= "__builtin_types_compatible_p"
BUILTIN_OFFSETOF ::= "__builtin_offsetof"
/* On some versions of GCC __thread is a regular identifier */
THREAD ::= "__thread"

ELLIPSIS ::= "..."
PLUS_EQ ::= "+="
MINUS_EQ ::= "-="
STAR_EQ ::= "*="
SLASH_EQ ::= "/="
PERCENT_EQ ::= "%="
PIPE_EQ ::= "|="
AND_EQ ::= "&="
CIRC_EQ ::= "^="
INF_INF_EQ ::= "<<="
SUP_SUP_EQ ::= ">>="
INF_INF ::= "<<"
SUP_SUP ::= ">>"
EQ_EQ ::= "=="
EXCLAM_EQ ::= "!="
INF_EQ ::= "<="
SUP_EQ ::= ">="
EQ ::= "="
INF ::= "<"
SUP ::= ">"
PLUS_PLUS  ::= "++"
MINUS_MINUS  ::= "--"
ARROW ::= "->"
PLUS  ::= '+'
MINUS  ::= '-'
STAR ::= '*'
SLASH ::= "/"
PERCENT ::= '%'
EXCLAM  ::= '!'
AND_AND  ::= "&&"
PIPE_PIPE ::= "||"
AND  ::= '&'
PIPE ::= '|'
CIRC ::= '^'
QUEST ::= '?'
COLON ::= ':'
TILDE  ::= '~'

LBRACE ::= '{'	| "<%"
RBRACE ::= '}'	| "%>"
LBRACKET ::= '['
RBRACKET ::= ']'
LBRACKET ::= "<:"
RBRACKET ::= ":>"
LPAREN ::= '('
RPAREN ::= ')'
SEMICOLON ::= ';'
COMMA ::= ','
DOT ::= '.'
SIZEOF ::= "sizeof"
MSASM ::= "__asm"

frama-c -wp -wp-rte -wp-gen -wp-prover cvc4 -wp-out find.wp find.c

/*@
  requires   \valid_read(a + (0..n-1));
  assigns    \nothing;
  ensures    0 <= \result <= n;

  behavior some:
    assumes  \exists integer i; 0 <= i < n && a[i] == val;
    assigns  \nothing;
    ensures  0 <= \result < n;
    ensures  a[\result] == val;
    ensures  \forall integer i; 0 <= i < \result ==> a[i] != val;

  behavior none:
    assumes  \forall integer i; 0 <= i < n ==> a[i] != val;
    assigns  \nothing;
    ensures  \result == n;

  complete behaviors;
  disjoint behaviors;
*/
unsigned int
find(const int* a, unsigned int n, int val)
{
  /*@
    loop invariant 0 <= i <= n;
    loop invariant \forall integer k; 0 <= k < i ==> a[k] != val;
    loop assigns i;
    loop variant n-i;
   */
  for (unsigned int i = 0u; i < n; i++) {
    if (a[i] == val) {
      return i;
    }
  }

  return n;
}

int main(int argc, char *argv[])
{
  size_t len;
  char src[4106];
  char buf[10];
  memset(src, 'A', 4106);
  src[4106 - 1] = '\0';
  len = 4106;
  strncpy(buf, src, len);
  return 0;
}

char buf[10];
src[4106 - 1] = '\0';
len = 4106;
strncpy(buf, src, len);

The following actions will be performed:
  - install frama-c 25.0

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> retrieved frama-c.25.0  (cached)
[ERROR] The compilation of frama-c.25.0 failed at "make -j11".

#=== ERROR while compiling frama-c.25.0 =======================================#
# context     2.1.3 | macos/x86_64 | ocaml-base-compiler.4.14.0 | https://opam.ocaml.org#cb4d2b35
# path        ~/.opam/4.14.0/.opam-switch/build/frama-c.25.0
# command     ~/.opam/opam-init/hooks/sandbox.sh build make -j11
# exit-code   2
# env-file    ~/.opam/log/frama-c-87828-262cb6.env
# output-file ~/.opam/log/frama-c-87828-262cb6.out
### output ###
# [...]
# Error: Unbound module Cil_types
# make: *** [share/Makefile.generic:78: src/plugins/aorai/logic_simplification.cmo] Error 2
# File "src/plugins/aorai/data_for_aorai.ml", line 26, characters 5-16:
# 26 | open Logic_ptree
#           ^^^^^^^^^^^
# Error: Unbound module Logic_ptree
# File "src/plugins/aorai/aorai_utils.ml", line 26, characters 5-8:
# 26 | open Cil
#           ^^^
# Error: Unbound module Cil
# make: *** [share/Makefile.generic:78: src/plugins/aorai/data_for_aorai.cmo] Error 2
# make: *** [share/Makefile.generic:78: src/plugins/aorai/aorai_utils.cmo] Error 2

<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build frama-c 25.0
+-
- No changes have been performed

<><> frama-c.25.0 troubleshooting <><><><><><><><><><><><><><><><><><><><><><><>
=> Why3 provers setup: rm -f ~/.why3.conf ; why3 config detect

#include <stdio.h>      /* printf, scanf, NULL */
#include <stdlib.h>

int main(int argc, char **argv) {
	int x = 1;
	int i = 0;
	for (; i < x; i = i + 2){
	    switch (i){
	         case 6:
	         L:
         x++;
	    }
	}
	if (x + 1 == i) {goto L;};	
	return x;  
}
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
int main(void)
{
  int x = 1;
  int i = 0;
  while (i < x) {
      L: case 6: x ++;
      i += 2;
  }
  if (x + 1 == i) goto L;
  return x;
}
/*@ 
  requires \valid(src);
  requires validDataBlockId(src);
*/
void IT_pack(IntervalTree * src, DatablockId dst);

goal WP[@expl:Instance of 'Pre-condition (file policy/intervalTree.h, line 57) in 'IT_pack'' in 'IT_add_datablock' at call 'IT_pack' (file policy/intervalTree.c, line 316)
]:

# Detecting depexts using vars: arch=x86_64, os=linux, os-distribution=ubuntu, os-family=debian
[ERROR] No solution for frama-c: The following dependencies couldn't be met:
          - frama-c → frama-c-base → ocaml < 4.06
              base of this switch (use `--unlock-base' to force)
          - frama-c → ocaml < 4.08.0
              base of this switch (use `--unlock-base' to force)

Command failed: opam list --readonly --external  --resolve=frama-c returned 20

The following actions will be performed:
  ∗  install why3-base 0.88.3                 [required by why3]
  ∗  install why3      0.88.3
       Coq realizations of Why3 theories are only available if Coq is installed
===== ∗  2 =====
Do you want to continue ? [Y/n] y

=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 
[why3-base] Archive in cache

=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 
[ERROR] The compilation of why3-base failed at "make -j4 all opt byte".
Processing  1/2: [why3-base: rm]
#=== ERROR while installing why3-base.0.88.3 ==================================#
# opam-version 1.2.2
# os           darwin
# command      make -j4 all opt byte
# path         /Users/wenlongxie/.opam/system/build/why3-base.0.88.3
# compiler     system (4.06.1)
# exit-code    2
# env-file     /Users/wenlongxie/.opam/system/build/why3-base.0.88.3/why3-base-7673-e7966f.env
# stdout-file  /Users/wenlongxie/.opam/system/build/why3-base.0.88.3/why3-base-7673-e7966f.out
# stderr-file  /Users/wenlongxie/.opam/system/build/why3-base.0.88.3/why3-base-7673-e7966f.err
### stdout ###
# [...]
# Ocamlc   src/printer/simplify.mli
# Ocamlc   src/printer/gappa.mli
# Ocamlc   src/printer/cvc3.mli
# Ocamlc   src/whyml/mlw_main.mli
# Ocamlc   src/session/compress.mli
# Ocamlc   src/session/xml.mli
# Ocamlc   src/util/bigInt.ml
# Ocamlc   src/util/util.ml
# Ocamlc   src/util/opt.ml
# Ocamlc   src/util/lists.ml
### stderr ###
# [...]
# Warning: you are using the standard library and/or the %inline keyword. We
# recommend switching on --infer in order to avoid obscure type error messages.
# Warning: you are using the standard library and/or the %inline keyword. We
# recommend switching on --infer in order to avoid obscure type error messages.
# Warning: you are using the standard library and/or the %inline keyword. We
# recommend switching on --infer in order to avoid obscure type error messages.
# File "src/util/bigInt.ml", line 12, characters 5-12:
# Error: Unbound module Big_int
# make: *** [src/util/bigInt.cmo] Error 2
# make: *** Waiting for unfinished jobs....

=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 
The following actions were aborted
  ∗  install why3 0.88.3
The following actions failed
  ∗  install why3-base 0.88.3
No changes have been performed

result ∈ [0x0.0000000000000p-1022 .. 0x1.0000000000000p4]

#ifdef FRAMA_C
    #include "__fc_builtin.h"
#else
    #include <stdio.h>
#endif

#define FLT_MAX 0xFFFFFEp+127

void add(float x, float y, float *result){
    double xDouble = 0, yDouble = 0, tmp = 0;

    xDouble = (double)x;
    yDouble = (double)y;
    tmp = xDouble + yDouble;

    if ( tmp < (double)-FLT_MAX )
    {
        *result = -FLT_MAX;
    }else if (tmp > (double)FLT_MAX )
    {
        *result = FLT_MAX;
    }else
    {
        *result = (float)tmp;
    }
}

int main( void ){

#ifdef FRAMA_C
    float x = Frama_C_float_interval(0x1.0p2, 0x1.4p4),
#else
    float x = 0x1.0p2,
#endif
    y = -0x1.0p2,
    result = 0;

    add(x, y, &result);

#ifndef FRAMA_C
    printf("Result:\t%a\n", result); 
#endif
}
printf "Example compiling\n\n" > log.txt
gcc -o main example.c
printf "\n" >> log.txt

printf "Example execution\n\n" >> log.txt
./main >> log.txt
printf "\n" >> log.txt

printf "EVA ANALYSIS\n\n" >> log.txt
frama-c -cpp-extra-args="-D FRAMA_C" -eva -float-hex example.c >> log.txt
Example compiling

Example execution

Result:	0x0p+0

EVA ANALYSIS

[kernel] Parsing example.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization

[eva] using specification for function Frama_C_float_interval
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function add2:
  xDouble ∈ [0x1.0000000000000p2 .. 0x1.4000000000000p4]
  yDouble ∈ {-0x1.0000000000000p2}
  tmp ∈ [0x0.0000000000000p-1022 .. 0x1.0000000000000p4]
  result ∈ [0x0.0000000000000p-1022 .. 0x1.0000000000000p4]
[eva:final-states] Values at end of function main:
  Frama_C_entropy_source ∈ [--..--]
  x ∈ [0x1.0000000000000p2 .. 0x1.4000000000000p4]
  y ∈ {-0x1.0000000000000p2}
  result ∈ [0x0.0000000000000p-1022 .. 0x1.0000000000000p4]
  __retres ∈ {0}
[eva:summary] ====== ANALYSIS SUMMARY ======
  ----------------------------------------------------------------------------
  2 functions analyzed (out of 2): 100% coverage.
  In these functions, 16 statements reached (out of 18): 88% coverage.
  ----------------------------------------------------------------------------
  No errors or warnings raised during the analysis.
  ----------------------------------------------------------------------------
  0 alarms generated by the analysis.
  ----------------------------------------------------------------------------
  Evaluation of the logical properties reached by the analysis:
    Assertions        0 valid     0 unknown     0 invalid      0 total
    Preconditions     2 valid     0 unknown     0 invalid      2 total
  100% of the logical properties reached have been proven.
  ----------------------------------------------------------------------------

:=-=- Synchronising pinned packages =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 
[frama-c] /Users/wenlongxie/Downloads/TOOLS/ already up-to-date
The following actions will be performed:
  ∗  install frama-c 20171101*
       Coq can be used with the WP plug-in for proving interactively proof obligations

=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 
[frama-c.20171101] /Users/wenlongxie/Downloads/TOOLS/ already up-to-date

=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 
[ERROR] The compilation of frama-c failed at "sh -eux ./run_autoconf_if_needed.sh".
Processing  1/1: [frama-c: rm]
#=== ERROR while installing frama-c.20171101 ==================================#
# opam-version 1.2.2
# os           darwin
# command      sh -eux ./run_autoconf_if_needed.sh
# path         /Users/wenlongxie/.opam/4.05.0/build/frama-c.20171101
# compiler     4.05.0
# exit-code    1
# env-file     /Users/wenlongxie/.opam/4.05.0/build/frama-c.20171101/frama-c-1443-05296d.env
# stdout-file  /Users/wenlongxie/.opam/4.05.0/build/frama-c.20171101/frama-c-1443-05296d.out
# stderr-file  /Users/wenlongxie/.opam/4.05.0/build/frama-c.20171101/frama-c-1443-05296d.err
### stderr ###
# + '[' '!' -f configure ']'
# + autoconf
# autoconf: error: no input file

=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 
The following actions failed
  ∗  install frama-c 20171101
No changes have been performed

pl@pl-VirtualBox:~/frama-clang-0.0.7$ ./configure 
checking for frama-c-gui... yes
checking for Makefile.config.in... yes
frama_clang... yes
checking for g++... g++
checking whether the C++ compiler works... yes
checking for C++ compiler default output file name... a.out
checking for suffix of executables... 
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether we are using the GNU C++ compiler... yes
checking whether g++ accepts -g... yes
checking for camlp4o... yes
checking for clang... clang
checking for clang++... clang++
checking for llvm-config... llvm-config
checking for /usr/lib/llvm-6.0/include/clang... yes
checking LLVM version... 6.0.0: Good
configure: frama_clang: yes
configure: creating ./config.status
config.status: creating ./Makefile.config

pl@pl-VirtualBox:~/frama-clang-0.0.7$ make
Ocamlc       gen_ast
Fatal error: cannot load shared library dllunix
Reason: /home/pl/.opam/4.07.0/lib/ocaml/stublibs/dllunix.so: undefined symbol: caml_ba_element_size
File "gen_ast.ml", line 1:
Error: Error while running external preprocessor
Command line: camlp4o 'gen_ast.ml' > /tmp/ocamlpp66b132

make: *** 'intermediate_format_parser.ml'에서 필요한 'gen_ast' 타겟을 만들 규칙이 없습니다.  멈춤.

pl@pl-VirtualBox:~/frama-clang-0.0.7$ ocaml --version
The OCaml toplevel, version 4.07.0
pl@pl-VirtualBox:~/frama-clang-0.0.7$ opam --version
2.0.4
pl@pl-VirtualBox:~/frama-clang-0.0.7$ opam switch
#  switch  compiler                    description
   4.06.1  ocaml-base-compiler.4.06.1  4.06.1
→  4.07.0  ocaml-base-compiler.4.07.0  4.07.0

#include <assert.h>

#define ADD_ASSERT(MIN, MAX) \
    static_assert(MIN < MAX, "Min should be lower than MAX");

ADD_ASSERT(3, 5)

int main()
{
    return 0;
}

$ ./configure
checking for frama-c-gui... yes
checking for Makefile.config.in... yes
frama_clang... yes
checking for g++... g++
checking whether the C++ compiler works... yes
checking for C++ compiler default output file name... a.exe
checking for suffix of executables... .exe
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether we are using the GNU C++ compiler... yes
checking whether g++ accepts -g... yes
checking for camlp4o... yes
checking for clang... clang
checking for clang++... clang++
checking for llvm-config... llvm-config
checking for D:\llvm-project-master\llvm\build\Debug/include/clang... no
configure: WARNING: frama_clang disabled because clang dev headers not found.
configure: frama_clang: no
configure: creating ./config.status
config.status: creating ./Makefile.config
chmod: ./Makefile.config: new permissions are r--rw-r--, not r--r--r--`

checking for frama-c-gui... yes
checking for Makefile.config.in... yes
frama_clang... yes
checking for g++... g++
checking whether the C++ compiler works... yes
checking for C++ compiler default output file name... a.out
checking for suffix of executables... 
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether the compiler supports GNU C++... yes
checking whether g++ accepts -g... yes
checking for g++ option to enable C++11 features... none needed
checking for camlp5o... no
configure: WARNING: camlp5o not found.
configure: WARNING: frama_clang disabled because camlp5o missing.
checking for clang... clang
checking for clang++... clang++
checking for llvm-config... no
checking for llvm-config-12... no
checking for llvm-config-11... no
checking for llvm-config-10... llvm-config-10
configure: frama_clang: no
configure: creating ./config.status
config.status: creating ./Makefile.config

Generating   .Makefile.plugin.generated
Ocamlc       gen_ast
ocamlfind: /usr/lib/ocaml/ld.conf: No such file or directory
make: *** No rule to make target 'gen_ast', needed by 'intermediate_format_parser.ml'.  Stop.

Definition select {A B : Type}
  (m : farray A B) (k : A) : B := @Map.get A (whytype1 m) B (whytype2 m) m k.

/*@
	assigns \nothing;
	ensures 'a' <= c <= 'z' <==> \result == 1;
*/
int is_lower_alpha(char c) {
    return 'a' <= c && c <= 'z' ;
}

/*@
	assigns \nothing;
	ensures 'A' <= c <= 'Z' <==> \result == 1;
*/
int is_upper_alpha(char c) {
    return 'A' <= c && c <= 'Z' ;
}

/*@
	assigns \nothing;
	ensures '0' <= c <= '9' <==> \result == 1;
*/
int is_digit(char c) {
    return '0' <= c && c <= '9' ;
}

/*@
	assigns \nothing;
	ensures ('a' <= c <= 'z' || 'A' <= c <= 'Z' || '0' <= c <= '9') <==> \result == 1;
*/
int is_alpha_num(char c) {
    return
        is_lower_alpha(c) ||
        is_upper_alpha(c) ||
        is_digit(c) ;
}

/*@
	assigns \nothing;
	ensures 'a' <= c <= 'z' <==> \result;
*/
int is_lower_alpha(char c) {
    return 'a' <= c && c <= 'z' ;
}

/*@
	assigns \nothing;
	ensures 'A' <= c <= 'Z' <==> \result;
*/
int is_upper_alpha(char c) {
    return 'A' <= c && c <= 'Z' ;
}

/*@
	assigns \nothing;
	ensures '0' <= c <= '9' <==> \result;
*/
int is_digit(char c) {
    return '0' <= c && c <= '9' ;
}

/*@
	assigns \nothing;
	ensures ('a' <= c <= 'z' || 'A' <= c <= 'Z' || '0' <= c <= '9') <==> \result;
*/
int is_alpha_num(char c) {
    return
        is_lower_alpha(c) ||
        is_upper_alpha(c) ||
        is_digit(c) ;
}

Fatal error: cannot load shared library dllunix
Reason: /usr/lib/ocaml/stublibs/dllunix.so: undefined symbol: caml_strdup```

frama-c / frama-c-snapshot Goto Github PK

frama-c-snapshot's Introduction

Note: The Official Frama-C Repository is now at our Gitlab!

A Collaborative Platform

Installation

Usage

Simple usage

Complex scenarios

Further reference

frama-c-snapshot's People

Contributors

Stargazers

Watchers

Forkers

frama-c-snapshot's Issues

find.c

Recommend Projects

Recommend Topics

Recommend Org

`find.c`