Project

General

Profile

« Previous | Next » 

Revision 9aa80a95

Added by Pierre-Loïc Garoche about 5 years ago

Example of integration of S-function code into Lustre.

View differences:

tests/external_code/mydouble/s_function/modif/Makefile
1
toto:
2
	lustrec -d build mydouble_wrapper.lusi
3
	cp mydouble.h build/
4
	cp mydouble.c build/
5
	cp mydouble_wrapper.c build/
6
	lustrec -d build -node ControlSys_SFunction example1.lus
7
	cp example1.makefile build/
8
	cd build; make -f example1.makefile
9

  
tests/external_code/mydouble/s_function/modif/Makefile~
1
toto:
2
	lustrec -d build mydouble_wrapper.lusi
3
	cp mydouble.h build/
4
	cp mydouble.c build/
5
	lustrec -d build -node ControlSys_SFunction example1.lus
tests/external_code/mydouble/s_function/modif/example1.lus
1
#open "mydouble_wrapper"
2
-- This file has been generated by CoCoSim
3

  
4

  
5
-- Extern nodes
6
node ControlSys_SFunction (in1_1: int; in2_1: int)
7
returns (SFunction_1_1: int)
8
let
9
	--! c_code: mydouble;
10
 
11
SFunction_1_1 = mydouble(in1_1, in2_1);
12

  
13
tel
14

  
15

  
16
-- Properties nodes
17
node example1_SafetyProp (In1_1_1 : int; In2_1_1 : int)
18
returns (Out1_1_1 : bool);
19
var
20
	LogicalOperator_1_1 : bool;
21
	RelationalOperator_1_1 : bool;
22
	In5_1_1 : int;
23
	i_virtual_local : real;
24
let
25
	LogicalOperator_1_1 = RelationalOperator_1_1 and (In5_1_1 != 0);
26
	RelationalOperator_1_1 = In1_1_1 >= In2_1_1;
27
	Out1_1_1 = LogicalOperator_1_1;
28
	i_virtual_local= 0.0 -> 1.0;
29

  
30
	In5_1_1 = example1(In2_1_1, In1_1_1);
31
	--%PROPERTY Out1_1_1; 
32
 
33
tel
34

  
35

  
36
-- System nodes
37
node example1 (In1_1_1 : int; In2_1_1 : int)
38
returns (Out1_1_1 : int); 
39
var
40
	ControlSys_SFunction_1_1 : int;
41
	ControlSys_System_RelationalOperator_1_1 : bool;
42
	ControlSys_System_Switch_1_1 : int;
43
	i_virtual_local : real;
44
let 
45
	(ControlSys_SFunction_1_1) = ControlSys_SFunction(In1_1_1, In2_1_1);
46
	ControlSys_System_RelationalOperator_1_1 = In1_1_1 >= ControlSys_SFunction_1_1;
47
	ControlSys_System_Switch_1_1 = if ControlSys_System_RelationalOperator_1_1 then In1_1_1 else ControlSys_SFunction_1_1;
48
	Out1_1_1 = ControlSys_System_Switch_1_1;
49
	i_virtual_local= 0.0 -> 1.0;
50
tel
51

  
tests/external_code/mydouble/s_function/modif/example1.makefile
1
GCC=gcc
2
LUSTREC=/home/ploc/Local/bin/lustrec
3
LUSTREC_BASE=/home/ploc/Local
4
INC=${LUSTREC_BASE}/include/lustrec
5

  
6
example1_ControlSys_SFunction: example1.c example1_main.c
7
	${GCC} -O0 -I${INC} -I. -c example1.c
8
	${GCC} -O0 -I${INC} -I. -c example1_main.c
9
	${GCC} -I${INC} -c ${INC}/io_frontend.c
10
	${GCC} -I${INC} -c mydouble.c mydouble_wrapper.c
11
	${GCC} -O0 -o example1_ControlSys_SFunction io_frontend.o mydouble.o mydouble_wrapper.o example1.o example1_main.o 
12

  
13
clean:
14
	\rm -f *.o example1_ControlSys_SFunction
15

  
16
.PHONY: example1_ControlSys_SFunction
17

  
18
FRAMACEACSL=`frama-c -print-share-path`/e-acsl
19
example1_eacsl.c: example1.c example1.h
20
	frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl example1.c -then-on e-acsl -print -ocode example1_eacsl.c
21

  
22

  
23
example1_main_eacsl.c: example1.c example1.h example1_main.c
24
	frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl example1.c example1_main.c -then-on e-acsl -print -ocode example1_main_eacsl.i
25
	grep -v _fc_stdout example1_main_eacsl.i > example1_main_eacsl.c
26

  
27
example1_main_eacsl: example1_main_eacsl.c
28
	${GCC} -Wno-attributes -I${INC} -I. -c example1_main_eacsl.c
29
	${GCC} -I${INC} -c ${INC}/io_frontend.c
30
	${GCC} -I${INC} -c mydouble_wrapper.c
31
	${GCC} -Wno-attributes -o example1_main_eacsl io_frontend.o mydouble_wrapper.o ${FRAMACEACSL}/e_acsl.c ${FRAMACEACSL}/memory_model/e_acsl_bittree.c ${FRAMACEACSL}/memory_model/e_acsl_mmodel.c example1_main_eacsl.o 
32

  
33

  
tests/external_code/mydouble/s_function/modif/mydouble.c
1
#include "mydouble.h"
2
int mydouble(int u, int w)
3
{
4
  return(u*w);
5
}
tests/external_code/mydouble/s_function/modif/mydouble.h
1
#ifndef _MYDOUBLE_H_
2
#define _MYDOUBLE_H_
3
int mydouble(int u, int w);
4
#endif
tests/external_code/mydouble/s_function/modif/mydouble.m
1
% Create the Legacy Code Tool data structure
2
def = legacy_code('initialize');
3

  
4
% Populate the data struture
5
def.SourceFiles = {'mydouble.c'};
6
def.HeaderFiles = {'mydouble.h'};
7
def.SFunctionName = 'legacy_mydouble';
8
def.OutputFcnSpec = 'int8 y1 = mydouble(int8 u1, int8 u2)';
9
def.SampleTime = [-1,0];
10

  
11

  
12
% Generate the S-function
13
legacy_code('sfcn_cmex_generate', def);
14

  
15
% Compile the MEX-file
16
legacy_code('compile', def);
17

  
18
% Generate a TLC-file
19
legacy_code('sfcn_tlc_generate', def);
tests/external_code/mydouble/s_function/modif/mydouble_wrapper.c
1
#include "mydouble.h"
2
void mydouble_step (int in1, int in2, int* out) {
3
	*out =	mydouble(in1, in2);
4
}
tests/external_code/mydouble/s_function/modif/mydouble_wrapper.lusi
1
function mydouble (u: int; w: int) returns (out: int) prototype c;
tests/external_code/mydouble/s_function/modif2/Makefile
1
toto:
2
	lustrec -d build mydouble_wrapper.lusi
3
	cp mydouble.h build/
4
	cp mydouble.c build/
5
	cp mydouble_wrapper.c build/
6
	lustrec -d build -node example1_SafetyProp example1.lus
7
	cp example1.makefile build
8
	cd build; make -f example1.makefile
tests/external_code/mydouble/s_function/modif2/Makefile~
1
toto:
2
	lustrec -d build mydouble_wrapper.lusi
3
	cp mydouble.h build/
4
	cp mydouble.c build/
5
	cp mydouble_wrapper.c build/
6
	lustrec -d build -node ControlSys_SFunction example1.lus
tests/external_code/mydouble/s_function/modif2/example1.lus
1
#open "mydouble_wrapper"
2
-- This file has been generated by CoCoSim
3

  
4
-- Properties nodes
5
node example1_SafetyProp (In1_1_1 : int; In2_1_1 : int)
6
returns (Out1_1_1 : bool);
7
var
8
	LogicalOperator_1_1 : bool;
9
	RelationalOperator_1_1 : bool;
10
	In5_1_1 : int;
11
	i_virtual_local : real;
12
let
13
	LogicalOperator_1_1 = RelationalOperator_1_1 and (In5_1_1 != 0);
14
	RelationalOperator_1_1 = In1_1_1 >= In2_1_1;
15
	Out1_1_1 = LogicalOperator_1_1;
16
	i_virtual_local= 0.0 -> 1.0;
17

  
18
	In5_1_1 = example1(In2_1_1, In1_1_1);
19
	--%PROPERTY Out1_1_1; 
20
 
21
tel
22

  
23

  
24
-- System nodes
25
node example1 (In1_1_1 : int; In2_1_1 : int)
26
returns (Out1_1_1 : int); 
27
var
28
	ControlSys_SFunction_1_1 : int;
29
	ControlSys_System_RelationalOperator_1_1 : bool;
30
	ControlSys_System_Switch_1_1 : int;
31
	i_virtual_local : real;
32
let 
33
	(ControlSys_SFunction_1_1) = ControlSys_SFunction(In1_1_1, In2_1_1);
34
	ControlSys_System_RelationalOperator_1_1 = In1_1_1 >= ControlSys_SFunction_1_1;
35
	ControlSys_System_Switch_1_1 = if ControlSys_System_RelationalOperator_1_1 then In1_1_1 else ControlSys_SFunction_1_1;
36
	Out1_1_1 = ControlSys_System_Switch_1_1;
37
	i_virtual_local= 0.0 -> 1.0;
38
tel
39

  
tests/external_code/mydouble/s_function/modif2/example1.lus~
1
#open "mydouble_wrapper"
2
-- This file has been generated by CoCoSim
3

  
4

  
5
-- Extern nodes
6
node ControlSys_SFunction (in1_1: int; in2_1: int)
7
returns (SFunction_1_1: int)
8
let
9
	--! c_code: mydouble;
10
 
11
SFunction_1_1 = mydouble(in1_1, in2_1);
12

  
13
tel
14

  
15

  
16
-- Properties nodes
17
node example1_SafetyProp (In1_1_1 : int; In2_1_1 : int)
18
returns (Out1_1_1 : bool);
19
var
20
	LogicalOperator_1_1 : bool;
21
	RelationalOperator_1_1 : bool;
22
	In5_1_1 : int;
23
	i_virtual_local : real;
24
let
25
	LogicalOperator_1_1 = RelationalOperator_1_1 and (In5_1_1 != 0);
26
	RelationalOperator_1_1 = In1_1_1 >= In2_1_1;
27
	Out1_1_1 = LogicalOperator_1_1;
28
	i_virtual_local= 0.0 -> 1.0;
29

  
30
	In5_1_1 = example1(In2_1_1, In1_1_1);
31
	--%PROPERTY Out1_1_1; 
32
 
33
tel
34

  
35

  
36
-- System nodes
37
node example1 (In1_1_1 : int; In2_1_1 : int)
38
returns (Out1_1_1 : int); 
39
var
40
	ControlSys_SFunction_1_1 : int;
41
	ControlSys_System_RelationalOperator_1_1 : bool;
42
	ControlSys_System_Switch_1_1 : int;
43
	i_virtual_local : real;
44
let 
45
	(ControlSys_SFunction_1_1) = ControlSys_SFunction(In1_1_1, In2_1_1);
46
	ControlSys_System_RelationalOperator_1_1 = In1_1_1 >= ControlSys_SFunction_1_1;
47
	ControlSys_System_Switch_1_1 = if ControlSys_System_RelationalOperator_1_1 then In1_1_1 else ControlSys_SFunction_1_1;
48
	Out1_1_1 = ControlSys_System_Switch_1_1;
49
	i_virtual_local= 0.0 -> 1.0;
50
tel
51

  
tests/external_code/mydouble/s_function/modif2/example1.makefile
1
GCC=gcc
2
LUSTREC=/home/ploc/Local/bin/lustrec
3
LUSTREC_BASE=/home/ploc/Local
4
INC=${LUSTREC_BASE}/include/lustrec
5

  
6
example1_example1_SafetyProp: example1.c example1_main.c
7
	${GCC} -O0 -I${INC} -I. -c example1.c
8
	${GCC} -O0 -I${INC} -I. -c example1_main.c
9
	${GCC} -I${INC} -c ${INC}/io_frontend.c
10
	${GCC} -I${INC} -c mydouble.c mydouble_wrapper.c
11
	${GCC} -O0 -o example1_example1_SafetyProp io_frontend.o mydouble.o mydouble_wrapper.o example1.o example1_main.o 
12

  
13
clean:
14
	\rm -f *.o example1_example1_SafetyProp
15

  
16
.PHONY: example1_example1_SafetyProp
17

  
18
FRAMACEACSL=`frama-c -print-share-path`/e-acsl
19
example1_eacsl.c: example1.c example1.h
20
	frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl example1.c -then-on e-acsl -print -ocode example1_eacsl.c
21

  
22

  
23
example1_main_eacsl.c: example1.c example1.h example1_main.c
24
	frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl example1.c example1_main.c -then-on e-acsl -print -ocode example1_main_eacsl.i
25
	grep -v _fc_stdout example1_main_eacsl.i > example1_main_eacsl.c
26

  
27
example1_main_eacsl: example1_main_eacsl.c
28
	${GCC} -Wno-attributes -I${INC} -I. -c example1_main_eacsl.c
29
	${GCC} -I${INC} -c ${INC}/io_frontend.c
30
	${GCC} -I${INC} -c mydouble_wrapper.c
31
	${GCC} -Wno-attributes -o example1_main_eacsl io_frontend.o mydouble_wrapper.o ${FRAMACEACSL}/e_acsl.c ${FRAMACEACSL}/memory_model/e_acsl_bittree.c ${FRAMACEACSL}/memory_model/e_acsl_mmodel.c example1_main_eacsl.o 
32

  
33

  
tests/external_code/mydouble/s_function/modif2/example1.makefile.bkp
1
GCC=gcc
2
LUSTREC=/home/ploc/Local/bin/lustrec
3
LUSTREC_BASE=/home/ploc/Local
4
INC=${LUSTREC_BASE}/include/lustrec
5

  
6
example1_ControlSys_SFunction: example1.c example1_main.c
7
	${GCC} -O0 -I${INC} -I. -c example1.c
8
	${GCC} -O0 -I${INC} -I. -c example1_main.c
9
	${GCC} -I${INC} -c ${INC}/io_frontend.c
10
	${GCC} -I${INC} -c mydouble.c mydouble_wrapper.c
11
	${GCC} -O0 -o example1_ControlSys_SFunction io_frontend.o mydouble.o mydouble_wrapper.o example1.o example1_main.o 
12

  
13
clean:
14
	\rm -f *.o example1_ControlSys_SFunction
15

  
16
.PHONY: example1_ControlSys_SFunction
17

  
18
FRAMACEACSL=`frama-c -print-share-path`/e-acsl
19
example1_eacsl.c: example1.c example1.h
20
	frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl example1.c -then-on e-acsl -print -ocode example1_eacsl.c
21

  
22

  
23
example1_main_eacsl.c: example1.c example1.h example1_main.c
24
	frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl example1.c example1_main.c -then-on e-acsl -print -ocode example1_main_eacsl.i
25
	grep -v _fc_stdout example1_main_eacsl.i > example1_main_eacsl.c
26

  
27
example1_main_eacsl: example1_main_eacsl.c
28
	${GCC} -Wno-attributes -I${INC} -I. -c example1_main_eacsl.c
29
	${GCC} -I${INC} -c ${INC}/io_frontend.c
30
	${GCC} -I${INC} -c mydouble_wrapper.c
31
	${GCC} -Wno-attributes -o example1_main_eacsl io_frontend.o mydouble_wrapper.o ${FRAMACEACSL}/e_acsl.c ${FRAMACEACSL}/memory_model/e_acsl_bittree.c ${FRAMACEACSL}/memory_model/e_acsl_mmodel.c example1_main_eacsl.o 
32

  
33

  
tests/external_code/mydouble/s_function/modif2/mydouble.c
1
#include "mydouble.h"
2
int mydouble(int u, int w)
3
{
4
  return(u*w);
5
}
tests/external_code/mydouble/s_function/modif2/mydouble.h
1
#ifndef _MYDOUBLE_H_
2
#define _MYDOUBLE_H_
3
int mydouble(int u, int w);
4
#endif
tests/external_code/mydouble/s_function/modif2/mydouble.m
1
% Create the Legacy Code Tool data structure
2
def = legacy_code('initialize');
3

  
4
% Populate the data struture
5
def.SourceFiles = {'mydouble.c'};
6
def.HeaderFiles = {'mydouble.h'};
7
def.SFunctionName = 'legacy_mydouble';
8
def.OutputFcnSpec = 'int8 y1 = mydouble(int8 u1, int8 u2)';
9
def.SampleTime = [-1,0];
10

  
11

  
12
% Generate the S-function
13
legacy_code('sfcn_cmex_generate', def);
14

  
15
% Compile the MEX-file
16
legacy_code('compile', def);
17

  
18
% Generate a TLC-file
19
legacy_code('sfcn_tlc_generate', def);
tests/external_code/mydouble/s_function/modif2/mydouble_wrapper.c
1
#include "mydouble.h"
2
void ControlSys_SFunction_step (int in1, int in2, int* out) {
3
	*out =	mydouble(in1, in2);
4
}
tests/external_code/mydouble/s_function/modif2/mydouble_wrapper.c~
1
#include "mydouble.h"
2
void mydouble_step (int in1, int in2, int* out) {
3
	*out =	mydouble(in1, in2);
4
}
tests/external_code/mydouble/s_function/modif2/mydouble_wrapper.lusi
1

  
2
-- Extern nodes
3

  
4
-- c_code: mydouble;	
5
function ControlSys_SFunction (in1_1: int; in2_1: int) returns (SFunction_1_1: int) prototype c;
tests/external_code/mydouble/s_function/modif2/mydouble_wrapper.lusi~
1
function mydouble (u: int; w: int) returns (out: int) prototype c;

Also available in: Unified diff