← Back to branch summary

~ubuntu-branches/debian/sid/frama-c/sid

« back to all changes in this revision

Viewing changes to tests/jessie/dassault_2.c

  • Committer: Bazaar Package Importer
  • Author(s): Mehdi Dogguy
  • Date: 2009-06-03 08:19:25 UTC
  • Revision ID: james.westby@ubuntu.com-20090603081925-kihvxvt0wy3zc4ar
Tags: upstream-20081201.dfsg
Import upstream version 20081201.dfsg

Show diffs side-by-side

added added

removed removed

Lines of Context:
tests/jessie/dassault_2.c
 
1
/**************************************************************************/
 
2
/*                                                                        */
 
3
/*  The Why/Caduceus/Krakatoa tool suite for program certification        */
 
4
/*  Copyright (C) 2002-2006                                               */
 
5
/*    Jean-Fran�ois COUCHOT                                               */
 
6
/*    Mehdi DOGGUY                                                        */
 
7
/*    Jean-Christophe FILLI�TRE                                           */
 
8
/*    Thierry HUBERT                                                      */
 
9
/*    Claude MARCH�                                                       */
 
10
/*    Yannick MOY                                                         */
 
11
/*                                                                        */
 
12
/*  This software is free software; you can redistribute it and/or        */
 
13
/*  modify it under the terms of the GNU General Public                   */
 
14
/*  License version 2, as published by the Free Software Foundation.      */
 
15
/*                                                                        */
 
16
/*  This software is distributed in the hope that it will be useful,      */
 
17
/*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
 
18
/*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  */
 
19
/*                                                                        */
 
20
/*  See the GNU General Public License version 2 for more details         */
 
21
/*  (enclosed in the file GPL).                                           */
 
22
/*                                                                        */
 
23
/**************************************************************************/
 
24
 
 
25
void g(
 
26
  int  Def_Rv
 
27
  );
 
28
 
 
29
 
 
30
typedef struct SCONT
 
31
{
 
32
  int        Def_Rv;
 
33
} SCONT;
 
34
 
 
35
/*@ requires Def_Rv == 1;*/
 
36
void g(
 
37
  int Def_Rv
 
38
);
 
39
 
 
40
void g (int Def_Rv){
 
41
  Def_Rv = 1;
 
42
}
 
43
 
 
44
 
 
45
/* 
 
46
Local Variables:
 
47
compile-command: "LC_ALL=C make dassault_2"
 
48
End:
 
49
*/