--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on March 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie failure: "Unexpected internal region in logic"



David Delmas wrote:
> Sorry, my last message was sent unfinished :
>
> Le vendredi 12 mars 2010 ? 10:48 +0100, David Delmas a ?crit :
>   
>> I don't know if it is any related, but I also just submitted a different
>> Jessie crash <http://bts.frama-c.com/view.php?id=426>.
>>     
>
> I would be happy to be shown a work-around to avoid this #426 crash.
> Indeed, it is blocking for my current experiments.
>
>   
Jessie does not like structures passed by value to logic functions and 
predicates. Please use extra pointers:

typedef struct {
    int index;
    char b;
} T_S;

//@ predicate P0{L}(T_S *s) = (s->b==1) ;

/*@ axiomatic Index {

logic integer f_index{L}(integer old, T_S *new);

// YYY ceci ne fait plus crasher Jessie  :-)

axiom Index1{L}:
    \forall integer old, T_S *new;
        P0{L}(new) ==> f_index{L}(old, new) == old;
}*/



-- 
Claude March?                          | tel: +33 1 72 92 59 69           
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93 
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29   
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |