Giter VIP home page Giter VIP logo

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

View Code? Open in Web Editor NEW
165.0 16.0 38.0 76.85 MB

Release snapshots of the Frama-C platform for source code analysis

Home Page: http://frama-c.com

Makefile 0.90% Shell 0.77% OCaml 73.41% Emacs Lisp 0.11% C++ 0.20% M4 0.27% C 17.82% Standard ML 0.02% Coq 1.75% Assembly 1.21% Python 0.28% HTML 0.01% Roff 0.31% Perl 0.19% SWIG 2.76%
c static-analysis runtime-verification ocaml formal-verification abstract-interpretation frama-c

frama-c-snapshot's Introduction

Frama-C

Frama-C is a platform dedicated to the analysis of source code written in C.

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

Frama-C has moved its official repository to our self-hosted Gitlab instance.

Official releases (starting from Frama-C 21) will no longer be updated here.

Nightly snapshots are also available in our Gitlab! You can now get access to the latest development version at: https://git.frama-c.com/pub/frama-c/-/tree/master

The official Frama-C issue tracker is now at our Gitlab: https://git.frama-c.com/pub/frama-c/-/issues

You can submit issues and pull requests using your Github login (choose "Sign in with Github" when prompted).

See you there!

A Collaborative Platform

Frama-C gathers several analysis techniques in a single collaborative platform, consisting of a kernel providing a core set of features (e.g., a normalized AST for C programs) plus a set of analyzers, called plug-ins. Plug-ins can build upon results computed by other plug-ins in the platform.

Thanks to this approach, Frama-C provides sophisticated tools, including:

  • an analyzer based on abstract interpretation, aimed at verifying the absence of run-time errors (Eva);
  • a program proof framework based on weakest precondition calculus (WP);
  • a program slicer (Slicing);
  • a tool for verification of temporal (LTL) properties (Aoraï);
  • a runtime verification tool (E-ACSL);
  • several tools for code base exploration and dependency analysis (From, Impact, Metrics, Occurrence, Scope, etc.).

These plug-ins share a common language and can exchange information via ACSL (ANSI/ISO C Specification Language) properties. Plug-ins can also collaborate via their APIs.

Installation

For more detailed information about installing OPAM/Frama-C, see INSTALL.md.

Frama-C is available through OPAM, the OCaml Package Manager. This is the preferred installation method. Be sure to install opam v2.0 or higher. Then the following sequence of commands should install frama-c and its gui:

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

Frama-C is developed mainly in Linux, often tested in macOS (via Homebrew), and occasionally tested on Windows (via the Windows Subsystem for Linux).

Usage

Frama-C can be run from the command-line, or via its graphical interface.

Simple usage

The recommended usage for simple files is one of the following lines:

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

Where -<plugin> is one of the several Frama-C plug-ins, e.g. -eva, or -wp, or -metrics, etc. Plug-ins can also be run directly from the GUI.

To list all plug-ins, run:

frama-c -plugins

Each plug-in has a help command (-<plugin>-help or -<plugin>-h) that describes its several options.

Finally, the list of options governing the behavior of Frama-C's kernel itself is available through

frama-c -kernel-help

Complex scenarios

For more complex usage scenarios (lots of files and directories, with several preprocessing directives), we recommend splitting Frama-C's usage in two parts:

  1. Parsing the input files and saving the result to a file;
  2. Loading the parsing results and then running the analyses or the GUI.

Parsing typically involves giving extra arguments to the C preprocessor, so the -cpp-extra-args option is often useful, as in the example below:

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

The results are then loaded into Frama-C for further analyses or for inspection via the GUI:

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

Further reference

  • Links to user and developer manuals, Frama-C archives, and plug-in manuals are available at
    http://frama-c.com/download.html

  • StackOverflow has several questions with the frama-c tag, which is monitored by several members of the Frama-C community.

  • The Frama-c-discuss mailing list is used for announcements and general discussions.

  • The official bug tracking system can be used for bug reports.

  • The Frama-C wiki has some useful information, although it is not entirely up-to-date.

  • The Frama-C blog has several posts about new developments of Frama-C, as well as general discussions about the C language, undefined behavior, floating-point computations, etc.

  • The Github snapshot repository contains the .tar.gz archives of stable Frama-C releases, ready to be cloned. It can also be used for reporting issues and submitting pull requests.

frama-c-snapshot's People

Contributors

bobot avatar dbuhle avatar maroneze avatar tantignac avatar vprevosto avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

frama-c-snapshot's Issues

program slicing

Hi! I am trying to use frama-c to get slicing of my code file.
My code file:

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

I want to use frama-c to get slicing like this:

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

I just want to keep the lines which are related to the callee:strncpy(buf, src, len);.
And are there some commands to automated get these lines even if there are more than one callees?

How launch the installed frama-c?

I have installed frama-c and its gui by running:
opam init
opam install depext
opam depext frama-c
opam install frama-c

$ opam show frama-c
package: frama-c
version: 20171101
$ opam list frama-c
Available packages for system:
frama-c 20171101 Platform dedicated to the analysis of source code written

But I run it, it tips errors as follow:
$ frama-c
The program 'frama-c' is currently not installed. You can install it by typing:
sudo apt install frama-c-base
$ frama-c-gui
The program 'frama-c-gui' is currently not installed. You can install it by typing:
sudo apt install frama-c

how can i launch the frama-c-gui?

[EVA] Unconventional hexadecimal display for 0

I found an unexpected hexadecimal display while using Frama-C version 20.0 (Calcium). Here's what I found :

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

As result is a single precision floating-point, it's exponent should be upper or equal than -127. This doesn't prevent from using Frama-C but it might hide another issue.

How to reproduce:

My C file example.c :

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

The small script I launched :

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

And the result:

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.
  ----------------------------------------------------------------------------

ACSL by Example on Argon beta

All experiments were conducted on a xubuntu-18.04 machine.

I was able to install Frama-C 18.0 (beta) with

  • opam 2.0.1
  • ocaml 4.05.0
  • why3 0.88.3 (which implies coq 8.7.2)

There are some minor changes in how the ACSL by Example code is verified but I had only to tweak one example to achieve complete verification.

Installation Issue

My env is macOS x86-64 Monterey 12.5.1
My opam version is 2.1.3, but when I install Frama-C, errors will be raise like

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

How to use option -wp-gen in Frama-C 20 ?

How does the option -wp-gen work in Frama-C 20?
Specifically, I would like to obtain the proof obligations for cvc4 (or the other supported provers) of the example find.c below.
I tried

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

but the directory find.wp is empty except for the empty subdirectory typed.

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

Prover 'alt-ergo' not found in why3.conf

Hello,

I know I should have asked on GitLab (I am waiting for approval), but I was hoping someone could help me here.

I am facing this issue using the latest version of Frama-C using opam. Below are the methods I tried to solve this issue:
-- why3 config detect: finds alt-ergo and the why3.conf contains the correct address
-- Manually add the alt-ergo to why3.conf using the add-prover command
-- The PATH is also updated and shows the correct directory of alt-ergo
-- Reinstall alt-ergo and why3
-- Check the execution permission for alt-ergo

I installed Frama-C on my Windows using WSL2 and Mint system followed the Frama-C website's instructions and got the same error.

Here are the current versions:
opam 2.1.2
ocaml 4.13.1
why3 1.7.1
alt-ergo 2.5.2

Below is what I get after trying running -wp:
[kernel] Parsing max.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] User Error: Prover 'alt-ergo' not found in why3.conf
[wp] Goal typed_max_ensures : not tried
[wp] Goal typed_max_ensures_2 : not tried
[wp:pedantic-assigns] max.c:6: Warning:
No 'assigns' specification for function 'max'.
Callers assumptions might be imprecise.
[wp] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Plug-in wp aborted: invalid user input.

a thought about loop variants

Here is a simple function that is verified with Frama-C without problems

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

If, however, the user accidentally types invariant instead of variant,
then Frama-C does not warn about it.
I don't hink this is a bug, although I think the "loop invariant" n-i looks a bit odd (as an aside the loop "invariant" is not verified (at least with alt-ergo)).

My point is, that it might be nice, if there were a way to warn a user that he did not specify a loop variant. Something along the lines -wp-check-termination.

Warnings while opening GUI : (Few items misplaced)

I use :
Linux kali 5.7.0-kali1-amd64 #1 SMP Debian 5.7.6-1kali2 (2020-07-01) x86_64 GNU/Linux
Theme is kinda dark.
So, when I launch Frama-c GUI,
It shows the following warnings:
`
** (frama-c-gui:20489): WARNING **: 13:48:57.056: Invalid borders specified for theme pixmap:
/usr/share/themes/Kali-Dark/gtk-2.0/assets/trough-scrollbar-horiz.png,
borders don't fit within the image

** (frama-c-gui:20489): WARNING **: 13:48:57.056: invalid source position for vertical gradient

** (frama-c-gui:20489): WARNING **: 13:48:57.056: invalid source position for vertical gradient

** (frama-c-gui:20489): WARNING **: 13:48:57.092: invalid source position for vertical gradient

** (frama-c-gui:20489): WARNING **: 13:48:57.092: invalid source position for vertical gradient

** (frama-c-gui:20489): WARNING **: 13:48:57.101: invalid source position for vertical gradient

** (frama-c-gui:20489): WARNING **: 13:48:57.101: invalid source position for vertical gradient`

Also I noticed problem with the span of menu drop-downs

framac-_gui_issue
and
framac-_gui_issue2

that in Analyses menu, the parameters are listed in black font with black background which makes difficult to read.
Also I fear that there may be few more issues.
Kindly look into it.

Program Slice

I know frama-c generates static program slices; however, I am wondering whether the slice of the program executable or not?

why3 not detecting

[Error:kernel] User Error: [findlib] package 'why3' not found (required by `frama-c-wp')
Versions:
Frama-c:20.0
why3:1.2.1
alt-ergo:2.0.0
opam-2.0.5

frama-clang install error: cannot shared library dllunix

Hi, i'm tyring to install frama-clang plugin now, but some error happen.

I use Ubuntu-18.04 and my opam, ocaml version is 2.0.4 and 4.07.0

I tried every bug Issue solution but 'make' command failed

my Log is here.

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

I guess the version is incompatible. but i can't fix this error. Could you help me?

Please let me know if you need any other information.

thanks.

Frama-C problem with ocaml 4.06.0

I am not sure this problem is particularly related to the Argon release but I would like to point it out anyway.

On xubuntu-18.04, with opam 2.0.1 and trying to execute the following steps

  • opam init --comp=4.06.0
  • opam install depext
  • opam depext frama-c

I receive the following error message.

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

Tool for extracting features/metrics from program dependency graphs of C code

I am a PG student and doing my research on code clone detection.
For this purpose I made program dependency graphs of C code using a tool named frama-c. Now I have to extract features/metrics from these program dependency graphs for further processing. Is there any tool that can extract features/metrics from program dependency graph.
Please help me in this issue ??

Frama-c requires Ocaml < 4.08

Followed installation instructions on ubuntu. After installing opam (2.0.5) and depext without problems, opam depext frama-c did not want to work and produced the following:

# 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

Turns out when installing opam, the version of ocaml installed automatically was 4.08.1. I was able to get frama-c in the end by downgrading ocaml (opam install ocaml.4.05.0 --unlock-base) but maybe it would be nice to make frama-c work with the latest version of ocaml.

program slicing

I am trying to use frama-c to get program slice. I've already read the doc http://frama-c.com/slicing.html. and I know there are many options to get program slice. I chose -slice-return to get my slicing. But I met error
my command :frama-c -slice-return main CWE114_Process_Control__w32_char_listen_socket_42.c
the error I met:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing CWE114_Process_Control__w32_char_listen_socket_42.c (with preprocessing)
CWE114_Process_Control__w32_char_listen_socket_42.c:136:[kernel] user error: syntax error
[kernel] user error: stopping on file "CWE114_Process_Control__w32_char_listen_socket_42.c" that
has errors. Add '-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.

I don't know how to fix it.would anyone give me some advice?

Frama-C/WP and Why3

Again, all remarks refer to xubuntu-18.04.

It looks like as if Frama-C/WP implicitly assumes that why3 is not newer than 0.88.3 and that coq is not newer 8.7.2.
If this is the case , then the installation of Frama-C should not allow the installation of newer, unsupported why3 versions.


The reason I assume this comes from the following observation.
If I don't pin why3 to 0.88.3 and thus install the most reason versions of why3 (1.1.0) and `coqide (8.8.2), then I receive later the warning

Found prover Coq version 8.8.2, but no Why3 libraries were compiled for it

WP: number of generated files in Frama-C 18 vs 19. beta(2)

There are some difficult to understand (internal) differences in the verification of the rotate_copy example from here.

Both 18.0 and 19 beta2 report the discharge of the 17 proof obligations of rotate_copy with reporting 5 discharged Qed and the remaining 12 by Alt-Ergo.

Frama-C 18.0 generates 12 .mlw and .out files.
Frama-C 19 beta2, on the other hand, only generates 9 .mlw and .out files.
The latter behaviour confuses our internal evaluation scripts which report that only 9 of the remaining 12 proof obligations have been discharged.

Different properties between Mac and Ubuntu

Hi, I followed this tutorial:
http://blog.frama-c.com/index.php?post/2017/03/17/A-simple-tutorial-part-two
both for Mac and ubuntu and the frama-c version is Chlorine.
First I did the operation frama-c test.c sha512.c monocypher.c -cpp-extra-args="-DED25519_SHA512" -save parsed.sav then frama-c -load parsed.sav -val -save value.sav(for -val-builtins-auto is built so I omitted it), at last I using gui to load it: frame-c-gui -load valued.sav.
But under Mac, the number of properties is 12, and for ubuntu this is about 900? What cause this problem? Thanks!
Sincerely

Result of conditional operator is 0 or 1

The following code fails to be verified when "frama-c-gui -wp -wp-timeout 100 -rte" is executed.

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

However, if we consider substituting all \result == 1 with just \result, then the prover succeeds. I don't get why since according to C standard the conditional operators yield either 1 or 0. Do I miss something? That is, the following is verified by WP:

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

[bug] Why3 translation bug on long descriptions

WP generates why3 files with goal with extra newlines (which makes why3 complain of syntax errors):

Example, for this statement:

/*@ 
  requires \valid(src);
  requires validDataBlockId(src);
*/
void IT_pack(IntervalTree * src, DatablockId dst);

I am getting generate call site asserts on the .why3 files that look like this:

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)
]:

The newline before the ] is invalid syntax on why3 1.2.0

This only happens when the line is long enough

Did Sulfur support ocaml 4.06.1 on mac os x

Hi, my os x version is 10.13.3, opam is 1.2.2 and ocaml is 4.06.1. Following the instructions, there was an error:

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

Has anyone tested for mac? Thanks!
Sincerely

unexpected text 'ite'

With Frama-C 20.0-beta, the cvc4-ce prover outputs strange and disturbing messages.
Here is a small and stupid demonstration :

$ frama-c -version
20.0-beta (Calcium)%

$ why3 --list-provers
Known provers:
Alt-Ergo 2.3.0
CVC4 1.6
CVC4 1.6 (counterexamples)
Z3 4.8.6
Z3 4.8.6 (counterexamples)
Z3 4.8.6 (noBV)

$ echo "/*@ ensures 1 == 2; */ void fo(){}" > bar.c

$ frama-c -wp -wp-prover cvc4 bar.c
[kernel] Parsing bar.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [CVC4 1.6] Goal typed_foo_ensures : Timeout (10s)
[wp] Proved goals: 0 / 1
CVC4 1.6: 0 (interrupted: 1)

$ frama-c -wp -wp-prover cvc4-ce bar.c
[kernel] Parsing bar.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] Waiting provers...File "Model string returned from the prover", line 1, characters 971-971:
warning: Error during parsing of smtlib model: unexpected text 'ite'
[wp] [CVC4 1.6 (counterexamples)] Goal typed_foo_ensures : Timeout (10s)
[wp] Proved goals: 0 / 1
CVC4 1.6 (counterexamples): 0 (interrupted: 1)

opam install frama-c on mac

There is the error as following

:=-=- 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

Maybe it was caused by opam pin add --kind=path frama-c

, I'm a little confused, thanks
Sincerely

Why3-1.x.x

I am trying to port wp to use why3-1.2.0, but it's kind of difficult because I am not familiar with why3. So one of the problems I found is that it fails to compile against why3, because why3-1.2.0 doesn't defines map.Map.get anymore (previously defined insided why3 on lib/coq/map/Map.v).
More specifically on src/plugins/wp/share/why3/Qedlib.v, this function is used:

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

Copying the function there is possible, but it's a hack and not a formalization; and also it breaks some proofs because I guess other theorems defined on why3 are not available anymore. Any thoughts on how to fix it?

Is there any planned release supporting this version of why3?

frama-clang failed to install

Hi,
I'm trying to install the Frama-Clang plugin on windows 10 following the instruction on the website. But the command

./configure

failed to execute and the messages are shown below:

$ ./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--`

I don't know how to solve this problem, any suggestions?

frama-c/wp and why3

Hello,

There appears to be an issue with some of the why3 files that get generated from user axiomatic definitions. I've installed frama-c using the nix-pkgs on the master branch, and hence have version 19.0, and why3 version 1.2.0.

/*@ axiomatic maps { type model_digit = octet | sextet; 
                     logic integer foo(model_digit i);
                   }
*/
int foo() {
//@assert \forall int i;  i == foo(octet);
  return 0;
}

Given the (silly) program above in simple.c, I get the following behavior

$ 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.

The A_maps.why file contains:

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

The error seems to be on the line (I'd imagine there should be an '=' but I am not a why3 user)

type a_model_digit | c_octet | c_sextet

Thanks!

frama-clang failed to install

Hi all,
I ran into the issue while installing frama-clang
I ran ./configure and get the following output

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

I guess ./configure run with no error, then i try to run make command as the documentation said and i ran in to the following error

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.

Please help me to resolve this error.
I have also refereed to the #10 issue but it didn't help me a lot.

non-compilable slice produced by frama-c

Hello, I've testing some unstructured programs to study how frama-c slicing plugin works, and I've found that the following code snippet produces a wrong (non-compilable) slice.

Program:

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

Frama-c Command:

frama-c code.c -then -eva -then -slice-return main -slicing-level 1 -slicing-keep-annotations -then-on 'Slicing export' -print -ocode slice.c

Output slice:

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

I would love to understand what went wrong in the slicing analysis, and if you got any references to the algorithm/technique in which the slicer plugin is based upon also would be highly appreciated.

How to generate Abstract Syntax Trees Using Frama-clang

I am a beginner in using frama-c. My operating system is Ubuntu. I have to generate Abstract syntax trees (ASTs) of C code using frama-clang. I do not know which commands have to used for generating ASTs from C source code. If anyone know about that please help me.

Have you ever tried Frama-C 20.0

I used Ubuntu 18.04.3 LTS for x86_64, opam 2.0.5, ocaml 4.05.0, why3 1.2.0, I found those problems:
1 Must install num, but it needs ocaml > 4.05
2 Which version of Coq should be used?
Could anyone can give some help? Thanks

Install frama-c issue

While installing frama-c using opam getting following errors

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

Grammar railroad diagram

I've done a experimental tool to convert bison grammars to a kind of EBNF understood by https://www.bottlecaps.de/rr/ui to generate railroad diagrams see bellow the converted src/kernel_internals/parsing/cparser.mly and with some hand made changes to allow view it at https://www.bottlecaps.de/rr/ui the order of the rules could be changed to a better view of the railroad diagrams. Copy and paste the EBNF bellow on https://www.bottlecaps.de/rr/ui tab Edit Grammar then switch to the tab View Diagram.

/*
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-clang failed to install

Hi,
I'm trying to install the Frama-Clang plugin following the instructions on the website. But the command

./configure

failed to execute and the messages are shown below:

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

I don't know how to solve this problem, any suggestions?

Frama-c not working with static_assert inside a macro

I am trying to use frama inside my program but I can't use it. My program uses macro with static_assert inside.

If there is the function static_assert(condition, message) (same problem with _Static_assert) inside a maccro I get an error from frama-c (syntax error). Everything is compiling fine with gcc 7.3.0 and I only have a issue with frama-c.

Am I doing something wrong? I've found nothing in the documentation relating this issue.

I use frama-c phosphorus-20170501.

An example is the code below:

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

I use the command:
frama-c main.c
The error message is:
[kernel] Frama-c aborted: invalid user input.
syntax error at main.c:6 (pointing the line with the maccro)

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.