Skip to content
Snippets Groups Projects
Commit d3a6265c authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl] Update tests

parent a3a64c43
No related branches found
No related tags found
No related merge requests found
Showing
with 19 additions and 20 deletions
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
int main(void)
{
int __retres;
......
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
int T1[3];
int T2[4];
void arrays(void)
......
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
extern int __e_acsl_sound_verdict;
int A = 0;
......
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
extern int __e_acsl_sound_verdict;
/*@ ensures
......
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
void f_signed(int a, int b)
{
int c = a << 2;
......
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
int main(void)
{
int __retres;
......
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
int main(void)
{
int __retres;
......
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
extern int __e_acsl_sound_verdict;
struct mystruct {
......
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
/*@ logic ℤ f1(ℤ n) = n ≤ 0? 0: f1(n - 1) + n;
*/
......
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
int main(void)
{
int __retres;
......
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
struct __anonstruct_r_1 {
int x ;
int y ;
......
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
unsigned long long my_pow(unsigned int x, unsigned int n)
{
unsigned long long __retres;
......
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
int main(void)
{
int __retres;
......
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
int main(void)
{
int __retres;
......
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
extern int __e_acsl_sound_verdict;
/*@ ensures \let delta = 1;
......
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
struct msgA {
int type ;
int a[2] ;
......
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
extern int __e_acsl_sound_verdict;
/*@ requires \valid(Mtmax_in);
......
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
extern int __e_acsl_sound_verdict;
/*@ behavior yes:
......
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
extern int __e_acsl_sound_verdict;
typedef int ArrayInt[5];
......
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
void duffcopy(char *to, char *from, int count)
{
__e_acsl_store_block((void *)(& from),(size_t)8);
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment