Grcov report - cb

1

// Do not edit this file as it will be overwritten if codegen is rerun

2

3

use data::*;

4

5

use proptest::prelude::*;

6

7

use super::test_apis::*;

8

9

use crate::bridge::thermostat_thermostat_GUMBOX as GUMBOX;

10

11

pub enum HarnessResult {

12

  RejectedPrecondition,

13

  FailedPostcondition(TestCaseError),

14

  Passed,

15

16

17

/** Contract-based test harness for the initialize entry point

18

*/

19

200

pub fn testInitializeCB() -> HarnessResult

20

200

21

200

  // [InvokeEntryPoint]: Invoke the entry point

22

200

  crate::thermostat_thermostat_initialize();

23

200

24

200

  // [RetrieveOutState]: retrieve values of the output ports via get operations and GUMBO declared local state variable

25

200

  let lastCmd = get_lastCmd();

26

200

  let api_heat_control = get_heat_control();

27

200

28

200

  // [CheckPost]: invoke the oracle function

29

200

  if !GUMBOX::initialize_IEP_Post (lastCmd, api_heat_control) {

30

    return HarnessResult::FailedPostcondition(

31

      TestCaseError::Fail("Postcondition failed: incorrect output behavior".into())

32

);

33

200

34

200

35

200

  return HarnessResult::Passed

36

200

37

38

#[macro_export]

39

macro_rules!

40

testInitializeCB_macro {

41

42

    $test_name: ident,

43

    config: $config:expr

44

  ) => {

45

    proptest!{

46

      #![proptest_config($config)]

47

      #[test]

48

      #[serial]

49

      fn $test_name(empty in ::proptest::strategy::Just(())) {

50

        match $crate::test::util::cb_apis::testInitializeCB() {

51

          $crate::test::util::cb_apis::HarnessResult::RejectedPrecondition => {

52

            unreachable!("This branch is infeasible")

53

54

          $crate::test::util::cb_apis::HarnessResult::FailedPostcondition(e) => {

55

            return Err(e)

56

57

          $crate::test::util::cb_apis::HarnessResult::Passed => { }

58

59

60

61

};

62

63

64

/** Contract-based test harness for the compute entry point

65

66

  * @param api_current_temp incoming data port

67

  * @param api_desired_temp incoming data port

68

*/

69

4

pub fn testComputeCB(

70

4

  api_current_temp: Isolette_Data_Model::Temp,

71

4

  api_desired_temp: Isolette_Data_Model::Set_Points) -> HarnessResult

72

4

73

4

  // Initialize the app

74

4

  crate::thermostat_thermostat_initialize();

75

4

76

4

  // [SaveInLocal]: retrieve and save the current (input) values of GUMBO-declared local state variables as retrieved

77

4

  //                from the component state

78

4

  let In_lastCmd: Isolette_Data_Model::On_Off = get_lastCmd();

79

4

80

4

  // [CheckPre]: check/filter based on pre-condition.

81

4

  if !GUMBOX::compute_CEP_Pre (In_lastCmd, api_current_temp, api_desired_temp) {

82

    return HarnessResult::RejectedPrecondition;

83

4

84

4

85

4

  // [PutInPorts]: Set values on the input ports

86

4

  put_current_temp(api_current_temp);

87

4

  put_desired_temp(api_desired_temp);

88

4

89

4

  // [InvokeEntryPoint]: Invoke the entry point

90

4

  crate::thermostat_thermostat_timeTriggered();

91

4

92

4

  // [RetrieveOutState]: retrieve values of the output ports via get operations and GUMBO declared local state variable

93

4

  let lastCmd = get_lastCmd();

94

4

  let api_heat_control = get_heat_control();

95

4

96

4

  // [CheckPost]: invoke the oracle function

97

4

  if !GUMBOX::compute_CEP_Post(In_lastCmd, lastCmd, api_current_temp, api_desired_temp, api_heat_control) {

98

    return HarnessResult::FailedPostcondition(TestCaseError::Fail("Postcondition failed: incorrect output behavior".into()));

99

4

100

4

101

4

  return HarnessResult::Passed

102

4

103

104

/** Contract-based test harness for the compute entry point

105

*/

106

2

pub fn testComputeCB_container(container: PreStateContainer) -> HarnessResult

107

2

108

2

  return testComputeCB(container.api_current_temp, container.api_desired_temp)

109

2

110

111

#[macro_export]

112

macro_rules!

113

testComputeCB_macro {

114

115

    $test_name: ident,

116

    config: $config:expr,

117

    api_current_temp: $api_current_temp_strat:expr,

118

    api_desired_temp: $api_desired_temp_strat:expr

119

  ) => {

120

    proptest!{

121

      #![proptest_config($config)]

122

      #[test]

123

      #[serial]

124

      fn $test_name(

125

        (api_current_temp, api_desired_temp)

126

            in ($api_current_temp_strat, $api_desired_temp_strat)

127

) {

128

        match$crate::test::util::cb_apis::testComputeCB(api_current_temp, api_desired_temp) {

129

          $crate::test::util::cb_apis::HarnessResult::RejectedPrecondition => {

130

            return Err(proptest::test_runner::TestCaseError::reject(

131

              "Precondition failed: invalid input combination",

132

))

133

134

          $crate::test::util::cb_apis::HarnessResult::FailedPostcondition(e) => {

135

            return Err(e)

136

137

          $crate::test::util::cb_apis::HarnessResult::Passed => { }

138

139

140

141

};

142

143

144

/** Contract-based test harness for the compute entry point

145

146

  * @param In_lastCmd pre-state state variable

147

  * @param api_current_temp incoming data port

148

  * @param api_desired_temp incoming data port

149

*/

150

290

pub fn testComputeCBwGSV(

151

290

  In_lastCmd: Isolette_Data_Model::On_Off,

152

290

  api_current_temp: Isolette_Data_Model::Temp,

153

290

  api_desired_temp: Isolette_Data_Model::Set_Points) -> HarnessResult

154

290

155

290

  // Initialize the app

156

290

  crate::thermostat_thermostat_initialize();

157

290

158

290

  // [CheckPre]: check/filter based on pre-condition.

159

290

  if !GUMBOX::compute_CEP_Pre (In_lastCmd, api_current_temp, api_desired_temp) {

160

88

    return HarnessResult::RejectedPrecondition;

161

202

162

202

163

202

  // [PutInPorts]: Set values on the input ports

164

202

  put_current_temp(api_current_temp);

165

202

  put_desired_temp(api_desired_temp);

166

202

167

202

  // [SetInStateVars]: set the pre-state values of state variables

168

202

  put_lastCmd(In_lastCmd);

169

202

170

202

  // [InvokeEntryPoint]: Invoke the entry point

171

202

  crate::thermostat_thermostat_timeTriggered();

172

202

173

202

  // [RetrieveOutState]: retrieve values of the output ports via get operations and GUMBO declared local state variable

174

202

  let lastCmd = get_lastCmd();

175

202

  let api_heat_control = get_heat_control();

176

202

177

202

  // [CheckPost]: invoke the oracle function

178

202

  if !GUMBOX::compute_CEP_Post(In_lastCmd, lastCmd, api_current_temp, api_desired_temp, api_heat_control) {

179

    return HarnessResult::FailedPostcondition(TestCaseError::Fail("Postcondition failed: incorrect output behavior".into()));

180

202

181

202

182

202

  return HarnessResult::Passed

183

290

184

185

/** Contract-based test harness for the compute entry point

186

*/

187

pub fn testComputeCBwGSV_container(container: PreStateContainer_wGSV) -> HarnessResult

188

189

  return testComputeCBwGSV(container.In_lastCmd, container.api_current_temp, container.api_desired_temp)

190

191

192

#[macro_export]

193

macro_rules!

194

testComputeCBwGSV_macro {

195

196

    $test_name: ident,

197

    config: $config:expr,

198

    In_lastCmd: $In_lastCmd_strat:expr,

199

    api_current_temp: $api_current_temp_strat:expr,

200

    api_desired_temp: $api_desired_temp_strat:expr

201

  ) => {

202

    proptest!{

203

      #![proptest_config($config)]

204

      #[test]

205

      #[serial]

206

      fn $test_name(

207

        (In_lastCmd, api_current_temp, api_desired_temp)

208

            in ($In_lastCmd_strat, $api_current_temp_strat, $api_desired_temp_strat)

209

) {

210

        match $crate::test::util::cb_apis::testComputeCBwGSV(In_lastCmd, api_current_temp, api_desired_temp) {

211

          $crate::test::util::cb_apis::HarnessResult::RejectedPrecondition => {

212

            return Err(proptest::test_runner::TestCaseError::reject(

213

              "Precondition failed: invalid input combination",

214

))

215

216

          $crate::test::util::cb_apis::HarnessResult::FailedPostcondition(e) => {

217

            return Err(e)

218

219

          $crate::test::util::cb_apis::HarnessResult::Passed => { }

220

221

222

223

};

224