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

pub fn testInitializeCB() -> HarnessResult

20

21

  // [InvokeEntryPoint]: Invoke the entry point

22

  crate::thermostat_thermostat_initialize();

23

24

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

25

  let lastCmd = get_lastCmd();

26

  let api_heat_control = get_heat_control();

27

28

  // [CheckPost]: invoke the oracle function

29

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

30

    return HarnessResult::FailedPostcondition(

31

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

32

);

33

34

35

  return HarnessResult::Passed

36

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

pub fn testComputeCB(

70

  api_current_temp: Isolette_Data_Model::Temp,

71

  api_desired_temp: Isolette_Data_Model::Set_Points) -> HarnessResult

72

73

  // Initialize the app

74

  crate::thermostat_thermostat_initialize();

75

76

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

77

  //                from the component state

78

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

79

80

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

81

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

82

    return HarnessResult::RejectedPrecondition;

83

84

85

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

86

  put_current_temp(api_current_temp);

87

  put_desired_temp(api_desired_temp);

88

89

  // [InvokeEntryPoint]: Invoke the entry point

90

  crate::thermostat_thermostat_timeTriggered();

91

92

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

93

  let lastCmd = get_lastCmd();

94

  let api_heat_control = get_heat_control();

95

96

  // [CheckPost]: invoke the oracle function

97

  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

100

101

  return HarnessResult::Passed

102

103

104

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

105

*/

106

pub fn testComputeCB_container(container: PreStateContainer) -> HarnessResult

107

108

  return testComputeCB(container.api_current_temp, container.api_desired_temp)

109

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

2

pub fn testComputeCBwGSV(

151

2

  In_lastCmd: Isolette_Data_Model::On_Off,

152

2

  api_current_temp: Isolette_Data_Model::Temp,

153

2

  api_desired_temp: Isolette_Data_Model::Set_Points) -> HarnessResult

154

2

155

2

  // Initialize the app

156

2

  crate::thermostat_thermostat_initialize();

157

2

158

2

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

159

2

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

160

    return HarnessResult::RejectedPrecondition;

161

2

162

2

163

2

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

164

2

  put_current_temp(api_current_temp);

165

2

  put_desired_temp(api_desired_temp);

166

2

167

2

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

168

2

  put_lastCmd(In_lastCmd);

169

2

170

2

  // [InvokeEntryPoint]: Invoke the entry point

171

2

  crate::thermostat_thermostat_timeTriggered();

172

2

173

2

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

174

2

  let lastCmd = get_lastCmd();

175

2

  let api_heat_control = get_heat_control();

176

2

177

2

  // [CheckPost]: invoke the oracle function

178

2

  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

2

181

2

182

2

  return HarnessResult::Passed

183

2

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