Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000456Frama-CPlug-in > jessiepublic2010-04-23 12:212010-04-23 12:21
Reportergava 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in Version 
Summary0000456: Lack of parameter generation
DescriptionThe 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"
Additional Informationtypedef 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);
TagsNo tags attached.
Attached Filesc file icon bspinprod.c [^] (3,355 bytes) 2010-04-23 12:21 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2010-04-23 12:21 gava New Issue
2010-04-23 12:21 gava Status new => assigned
2010-04-23 12:21 gava Assigned To => cmarche
2010-04-23 12:21 gava File Added: bspinprod.c


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker