merge parse_preconditions and parse_postconditions into parse_conditions

Author: mkovaxx

crates/anodized-core/src/annotate.rs

@@ -87,12 +87,12 @@ impl Parse for Spec {
                     }
                 }
                 Keyword::Requires => {
-                    if let Err(error) = arg.parse_preconditions(&mut requires) {
+                    if let Err(error) = arg.parse_conditions(&mut requires) {
                         errors.add(error);
                     }
                 }
                 Keyword::Maintains => {
-                    if let Err(error) = arg.parse_preconditions(&mut maintains) {
+                    if let Err(error) = arg.parse_conditions(&mut maintains) {
                         errors.add(error);
                     }
                 }
@@ -119,7 +119,7 @@ impl Parse for Spec {
                     }
                 }
                 Keyword::Ensures => {
-                    if let Err(error) = arg.parse_postconditions(&mut ensures) {
+                    if let Err(error) = arg.parse_conditions(&mut ensures) {
                         errors.add(error);
                     }
                 }
@@ -174,7 +174,7 @@ impl Parse for DataSpec {
                     ));
                 }
                 Keyword::Maintains => {
-                    if let Err(error) = arg.parse_preconditions(&mut maintains) {
+                    if let Err(error) = arg.parse_conditions(&mut maintains) {
                         errors.add(error);
                     }
                 }
@@ -217,7 +217,7 @@ impl Parse for LoopSpec {
                     ));
                 }
                 Keyword::Maintains => {
-                    if let Err(error) = arg.parse_preconditions(&mut maintains) {
+                    if let Err(error) = arg.parse_conditions(&mut maintains) {
                         errors.add(error);
                     }
                 }
@@ -284,23 +284,23 @@ impl SpecArg {
         Ok(())
     }
 
-    fn parse_preconditions(self, preconditions: &mut Vec<Condition>) -> Result<()> {
+    fn parse_conditions(self, conditions: &mut Vec<Condition>) -> Result<()> {
         let cfg_attr = find_cfg_attribute(&self.attrs)?;
         let cfg: Option<Meta> = if let Some(attr) = cfg_attr {
             Some(attr.parse_args()?)
         } else {
             None
         };
         let expr = self.value.try_into_expr()?;
-        if let Expr::Array(conditions) = expr {
-            for expr in conditions.elems {
-                preconditions.push(Condition {
+        if let Expr::Array(items) = expr {
+            for expr in items.elems {
+                conditions.push(Condition {
                     expr,
                     cfg: cfg.clone(),
                 });
             }
         } else {
-            preconditions.push(Condition { expr, cfg });
+            conditions.push(Condition { expr, cfg });
         }
         Ok(())
     }
@@ -340,27 +340,6 @@ impl SpecArg {
         Ok(())
     }
 
-    fn parse_postconditions(self, postconditions: &mut Vec<Condition>) -> Result<()> {
-        let cfg_attr = find_cfg_attribute(&self.attrs)?;
-        let cfg: Option<Meta> = if let Some(attr) = cfg_attr {
-            Some(attr.parse_args()?)
-        } else {
-            None
-        };
-        let expr = self.value.try_into_expr()?;
-        if let Expr::Array(conditions) = expr {
-            for expr in conditions.elems {
-                postconditions.push(Condition {
-                    expr,
-                    cfg: cfg.clone(),
-                });
-            }
-        } else {
-            postconditions.push(Condition { expr, cfg });
-        }
-        Ok(())
-    }
-
     fn parse_decreases(self, decreases: &mut Option<LoopVariant>) -> Result<()> {
         let cfg_attr = find_cfg_attribute(&self.attrs)?;
         let cfg: Option<Meta> = if let Some(attr) = cfg_attr {