/*undefined序列*/在Frama的切片代码中

Question

我试图使用Frama对代码进行切片。

源代码是

static uint8_T ALARM_checkOverInfusionFlowRate(void)
{
uint8_T ov;
ov = 0U;
if (ALARM_Functional_B.In_Therapy) {
  if (ALARM_Functional_B.Flow_Rate > ALARM_Functional_B.Flow_Rate_High) {
     ov = 1U;
   } else if (ALARM_Functional_B.Flow_Rate >
       ALARM_Functional_B.Commanded_Flow_Rate * div_s32
           (ALARM_Functional_B.Tolerance_Max, 100) +
                  ALARM_Functional_B.Commanded_Flow_Rate) {
                     ov = 1U;
                  } else {
                      if (ALARM_Functional_B.Flow_Rate > ALARM_Functional_B.Commanded_Flow_Rate *                div_s32(ALARM_Functional_B.Tolerance_Min, 100) + ALARM_Functional_B.Commanded_Flow_Rate) {
                         ov = 2U;
                      }
                }
      }
  return ov;
}

当我分割usig代码时，我得到以下内容。我不知道这个“未定义的序列”是什么意思。

static uint8_T ALARM_checkOverInfusionFlowRate(void)
{
  uint8_T ov;
  ov = 0U;
  if (ALARM_Functional_B.In_Therapy)
    if ((int)ALARM_Functional_B.Flow_Rate > (int)ALARM_Functional_B.Flow_Rate_High)
      ov = 1U;
    else {
      int32_T tmp_0;
      {
        /*undefined sequence*/
        tmp_0 = div_s32((int)ALARM_Functional_B.Tolerance_Max,100);
      }
      if ((int)ALARM_Functional_B.Flow_Rate > (int)ALARM_Functional_B.Commanded_Flow_Rate * tmp_0 + (int)ALARM_Functional_B.Commanded_Flow_Rate)
        ov = 1U;
      else {
        int32_T tmp;
        {
          /*undefined sequence*/
          tmp = div_s32((int)ALARM_Functional_B.Tolerance_Min,100);
        }
        if ((int)ALARM_Functional_B.Flow_Rate > (int)ALARM_Functional_B.Commanded_Flow_Rate * tmp + (int)ALARM_Functional_B.Commanded_Flow_Rate)
          ov = 2U;
      }
    }
  return ov;
}

感谢任何帮助解释为什么会发生这种情况。

Answer 1

块中的/* undefined sequence */仅仅意味着在解析时在代码规范化期间生成了块，但是在C语义方面，组成它的语句之间没有序列点。例如，x++ + x++将标准化为

 {
    /*undefined sequence*/
    tmp = x;
    x ++;
    tmp_0 = x;
    x ++;
    ;
 }

在内部，这样一个序列中的每个语句都被用于写入或读取的位置列表修饰(使用-kernel-debug 1和-print在输出中查看它们)。与-val一起使用的选项-val将检查这样的访问是否正确，也就是说，在写入给定位置的序列中最多有一条语句，如果是这样的话，则没有读取访问权限(除了构建分配给它的值之外)。此外，此选项不考虑在序列中的函数调用中发生的副作用。有一个特殊的插件，但它还没有发布。

最后，请注意，由于Frama，评论只读取/*sequence*/，这似乎不那么让用户望而却步。实际上，原始代码可能是正确的，或者可能显示出未定义的行为，但是语法分析太弱，无法在一般情况下决定。例如，(*p)++ + (*q)++是正确的，只要p和q不重叠。这就是为什么规范化阶段只指出序列，让更强大的分析插件来检查是否存在问题。