Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] unable to interprete and trace jessie's output errors

  • Subject: [Frama-c-discuss] unable to interprete and trace jessie's output errors
  • From: x_cui at hotmail.com (Xiao-lei Cui)
  • Date: Sun, 3 Nov 2013 22:45:29 -0500
Hi all,
    I embed some ACSL annotation in a small OS kernel source code. As I run frama-c -jessie over the entire source folder, I was unable to understand the output errors. It is possible I am doing it in a clumsy way, so any suggestion would be really appreciated!
    The script I run is:
/*-----------------start script--------------------*/
#!/bin/bash
OS_SRC=$HOME/projects/SZOS
FRAMA_C=frama-c
 
CPP_COMMAND="gcc -C -E -D_EM_WSIZE=4 -D_EM_PSIZE=4 -nostdinc -I$OS_SRC/h"

trav()
{
        for x in $(ls)
        do
                if [ -f "$x" ];then
                        echo "$x";
                elif [ -L "$x" ];then
                        echo "this is a link";
                else
                        cd "$x";
               pwd;
               frama-c -jessie -cpp-command 'gcc -C -E -nostdinc -I/home/cuix/projects/workspace/acsl_szos/h -I/home/cuix/projects/workspace/acsl_szos/h/kernel -DCPU=SPARC_V7' -pp-annot *.h;                      
              frama-c -jessie -cpp-command 'gcc -C -E -nostdinc -I/home/cuix/projects/workspace/acsl_szos/h -I/home/cuix/projects/workspace/acsl_szos/h/kernel -DCPU=SPARC_V7' -pp-annot *.c;
              trav;
              cd ..
                fi
        done
}
trav
/*-------------------end of shell script-------------------------*/   
    And in command line, I use to catch the output:
  $ ./trav 2>&1 out.txt 
    Part of the output looks like:
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir wholeprogram.jessie
[jessie] File wholeprogram.jessie/wholeprogram.jc written.
[jessie] File wholeprogram.jessie/wholeprogram.cloc written.
[jessie] Calling Jessie tool in subdir wholeprogram.jessie
Warning: recursive definition of reachable in generated file
Warning: recursive definition of reachable in generated file
Warning: recursive definition of reachable in generated file
[jessie] Calling VCs generator.
gwhy-bin [...] why/wholeprogram.why
Computation of VCs...
File "why/wholeprogram.why", line 69, characters 46-71:
Unbound variable dlnode_root_1_alloc_table
make: *** [wholeprogram.stat] Error 1
[jessie] user error: Jessie subprocess failed: make -f wholeprogram.makefile gui
[kernel] user error: source file "*.c" does not exist
[kernel] user error: skipping file "*.c" that has errors.
[kernel] Frama-C aborted because of invalid user input.
     It looks to me that jessie generates one .why file for each folder processed. The error comes from ACSL spec(so far the only ACSL spec I annotate) in some included header file:

    typedef struct dlnode
    {
        struct dlnode *next;
        struct dlnode *previous;
    } DL_NODE;

    typedef struct
    {
        DL_NODE *head;
        DL_NODE *tail;
    } DL_LIST;

 /*@
    inductive reachable (DL_NODE* root, DL_NODE* node) {
    case root_reachable:
    \forall DL_NODE* root; reachable(root,root);
    case next_reachable:
    \forall DL_NODE* root, *node;
    \valid(root) ==> reachable(root->next, node) ==>
    reachable(root,node);
    }
 @*/  

   However, I don't see errors from the quoted code above.  Any ideas what went wrong?
   Thank you.

xiaolei

   
 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131103/992ff788/attachment-0001.html>