Grcov report - thermostat_thermostat

1

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

2

3

use vstd::prelude::*;

4

use data::*;

5

use super::extern_c_api as extern_api;

6

7

verus! {

8

  pub trait thermostat_thermostat_Api {}

9

10

  pub trait thermostat_thermostat_Put_Api: thermostat_thermostat_Api {

11

    #[verifier::external_body]

12

    fn unverified_put_heat_control(

13

12

      &mut self,

14

12

      value: Isolette_Data_Model::On_Off)

15

12

16

12

      extern_api::unsafe_put_heat_control(&value);

17

12

18

19

20

  pub trait thermostat_thermostat_Get_Api: thermostat_thermostat_Api {

21

    #[verifier::external_body]

22

4

    fn unverified_get_current_temp(

23

4

      &mut self,

24

4

      value: &Ghost<Isolette_Data_Model::Temp>) -> (res : Isolette_Data_Model::Temp)

25

4

      ensures

26

4

        res == value@,

27

4

        // assume ASSM_CT_Range

28

4

        (crate::component::thermostat_thermostat_app::Temp_Lower_Bound() <= res.degrees) &&

29

4

          (res.degrees <= crate::component::thermostat_thermostat_app::Temp_Upper_Bound()),

30

4

31

4

      return extern_api::unsafe_get_current_temp();

32

4

33

34

    #[verifier::external_body]

35

4

    fn unverified_get_desired_temp(

36

4

      &mut self,

37

4

      value: &Ghost<Isolette_Data_Model::Set_Points>) -> (res : Isolette_Data_Model::Set_Points)

38

4

      ensures

39

4

        res == value@,

40

4

41

4

      return extern_api::unsafe_get_desired_temp();

42

4

43

44

45

  pub trait thermostat_thermostat_Full_Api: thermostat_thermostat_Put_Api + thermostat_thermostat_Get_Api {}

46

47

  pub struct thermostat_thermostat_Application_Api<API: thermostat_thermostat_Api> {

48

    pub api: API,

49

50

    pub ghost current_temp: Isolette_Data_Model::Temp,

51

    pub ghost desired_temp: Isolette_Data_Model::Set_Points,

52

    pub ghost heat_control: Isolette_Data_Model::On_Off

53

54

55

  impl<API: thermostat_thermostat_Put_Api> thermostat_thermostat_Application_Api<API> {

56

12

    pub fn put_heat_control(

57

12

      &mut self,

58

12

      value: Isolette_Data_Model::On_Off)

59

12

      ensures

60

12

        old(self).current_temp == self.current_temp,

61

12

        old(self).desired_temp == self.desired_temp,

62

12

        self.heat_control == value,

63

12

64

12

      self.api.unverified_put_heat_control(value);

65

12

      self.heat_control = value;

66

12

67

68

69

  impl<API: thermostat_thermostat_Get_Api> thermostat_thermostat_Application_Api<API> {

70

4

    pub fn get_current_temp(&mut self) -> (res : Isolette_Data_Model::Temp)

71

4

      ensures

72

4

        old(self).current_temp == self.current_temp,

73

4

        res == self.current_temp,

74

4

        old(self).desired_temp == self.desired_temp,

75

4

        old(self).heat_control == self.heat_control,

76

4

        // assume ASSM_CT_Range

77

4

        (crate::component::thermostat_thermostat_app::Temp_Lower_Bound() <= res.degrees) &&

78

4

          (res.degrees <= crate::component::thermostat_thermostat_app::Temp_Upper_Bound()),

79

4

80

4

      self.api.unverified_get_current_temp(&Ghost(self.current_temp))

81

4

82

4

    pub fn get_desired_temp(&mut self) -> (res : Isolette_Data_Model::Set_Points)

83

4

      ensures

84

4

        old(self).current_temp == self.current_temp,

85

4

        old(self).desired_temp == self.desired_temp,

86

4

        res == self.desired_temp,

87

4

        old(self).heat_control == self.heat_control,

88

4

89

4

      self.api.unverified_get_desired_temp(&Ghost(self.desired_temp))

90

4

91

92

93

  pub struct thermostat_thermostat_Initialization_Api;

94

  impl thermostat_thermostat_Api for thermostat_thermostat_Initialization_Api {}

95

  impl thermostat_thermostat_Put_Api for thermostat_thermostat_Initialization_Api {}

96

97

  pub const fn init_api() -> thermostat_thermostat_Application_Api<thermostat_thermostat_Initialization_Api> {

98

    return thermostat_thermostat_Application_Api {

99

      api: thermostat_thermostat_Initialization_Api {},

100

101

      current_temp: Isolette_Data_Model::Temp { degrees: 0 },

102

      desired_temp: Isolette_Data_Model::Set_Points { lower: Isolette_Data_Model::Temp { degrees: 0 }, upper: Isolette_Data_Model::Temp { degrees: 0 } },

103

      heat_control: Isolette_Data_Model::On_Off::Onn

104

105

106

107

  pub struct thermostat_thermostat_Compute_Api;

108

  impl thermostat_thermostat_Api for thermostat_thermostat_Compute_Api {}

109

  impl thermostat_thermostat_Put_Api for thermostat_thermostat_Compute_Api {}

110

  impl thermostat_thermostat_Get_Api for thermostat_thermostat_Compute_Api {}

111

  impl thermostat_thermostat_Full_Api for thermostat_thermostat_Compute_Api {}

112

113

  pub const fn compute_api() -> thermostat_thermostat_Application_Api<thermostat_thermostat_Compute_Api> {

114

    return thermostat_thermostat_Application_Api {

115

      api: thermostat_thermostat_Compute_Api {},

116

117

      current_temp: Isolette_Data_Model::Temp { degrees: 0 },

118

      desired_temp: Isolette_Data_Model::Set_Points { lower: Isolette_Data_Model::Temp { degrees: 0 }, upper: Isolette_Data_Model::Temp { degrees: 0 } },

119

      heat_control: Isolette_Data_Model::On_Off::Onn

120

121

122