Frama-C Bug Tracking System - Frama-C
View Issue Details
0000456Frama-CPlug-in > jessiepublic2010-04-23 12:212010-04-23 12:21
gava 
cmarche 
normalminoralways
assignedopen 
Frama-C Boron-20100401 
 
0000456: Lack of parameter generation
The following program (even if there are not enought annotations) works with Frama-C Berylium (with why-2.23) but crashes with Boron/why-2.24

The VC of WHY is launched and it said that a parameter is missing... The pb does not arise with why-2.23/Brylium

Frédéric G.

ps: the file "bsp.h" in the "additional information"

pps : I used "frama-c -jessie bspinprod.c"
typedef value_type;

/*@
 axiomatic GoodNumberProcessor
 {
  logic integer bsp_p;
  axiom good_bsp_p: 0<bsp_p;
 }
*/

/*@
 ensures \result==bsp_p;
*/
int bsp_nprocs();

/*@
 ensures 0<=\result<bsp_p;
*/
int bsp_pid();

int bsp_l();

int bsp_g();

int bsp_r();

/*@
 assigns \nothing;
*/
void bsplib_init(int* argc, char*** argv);

void bsplib_done();

double bsp_time();

void bsp_sync();

/* void bsp_push_reg(void* ident, int size); */

/*@
 assigns \nothing;
*/
void bsp_push_reg(value_type* ident, int n);

/* void bsp_pop_reg(void* ident); */

/*@
 assigns \nothing;
*/
void bsp_pop_reg(value_type* ident);

/* void bsp_put(int destPID, void* src, void* dest, int offset, int nbytes); */
/*@
 assigns \nothing;
*/
void bsp_put(int destPID, value_type* src, value_type* dest, int offset, int nbytes);

/* void bsp_get(int srcPID, value_type* src, int offset, value_type* dest, int nbytes); */
/*@
 assigns \nothing;
*/
void bsp_get(int srcPID, value_type* src, int offset, void* dest, int nbytes);

/* void bsp_send(int dest, void* buffer, int size); */
/*@
 assigns \nothing;
*/
void bsp_send(int dest, value_type* buffer, int size);

/* void* bsp_getmsg(int proc_id, int index); */
/*@
 assigns \nothing;
*/
value_type *bsp_getmsg(int proc_id, int index);

/*@
 assigns \nothing;
*/
int bspmsg_size(int proc_id, int index);

/*@
 assigns \nothing;
*/
int bsp_nmsgs(int proc_id);
No tags attached.
c bspinprod.c (3,355) 2010-04-23 12:21
https://bts.frama-c.com/file_download.php?file_id=78&type=bug
Issue History
2010-04-23 12:21gavaNew Issue
2010-04-23 12:21gavaStatusnew => assigned
2010-04-23 12:21gavaAssigned To => cmarche
2010-04-23 12:21gavaFile Added: bspinprod.c

There are no notes attached to this issue.