如何验证两份不同风格的C语言代码是否等价？

两份待验证的代码 #

Style 1 #

#include <stdio.h>
#define K1 42
#define K2 1200

int i1, i2, i3 = -10;
unsigned u1, u2 = 1230, u3 = K1, u4;

int main( void ) {
    
    scanf( "%d", &i2 );
    scanf( "%u", &u1 );
    for ( i1 = i2 - 1; i2 < i3-i1 || u2 >= u1; u2 = u3, u3 = u3 % ++u4 ) {
        i2 = i2 / 2 + i3++;
        scanf( "%u", &u4 );
        do {
            i3 -= K2;
            u4 = ( u4 << 2 ) & ~ 0x04;
            i1 = i3 / i2;
        } while ( u4 < K1 && i1 + 23 >= i2 + 4 );
        u3 = --u1 + ( u4 -= 2);
    }
    u1 = ( u4 - u2 ) * 5 + ( u2 + u3 ) / 6 - u1;
    
    return 0;
}

Style 2 #

#include <stdio.h>
#define K1 42
#define K2 1200

int i1 = 0;
int i2 = 0;
int i3 = -10;
int t;
unsigned u1 = 0;
unsigned u2 = 1230;
unsigned u3 = K1;
unsigned u4 = 0 ;

int main(){

    scanf( "%d", &i2 );
    scanf( "%d", &u1 );
    i1 = i2 - 1;
    t = i3 - i1;
    
for_beg:
    if ( i2 < t ) goto for_tt;
    if ( u2 >= u1 ) goto for_tt;
    goto for_ff;

for_tt:
    i2 = i2 / 2;
    i2 += i3;
    i3 += 1;
    scanf( "%u", &u4 );
    
do_begin:
    i3 -= K2;
    u4 = u4 << 2;
    u4 = ~ 0x04;
    i1 = i3 / i2;
    
while_beg:
    if ( u4 >= K1 ) goto while_ff;
    t = i1 + 23;
    int t2 = i2 + 4;
    if ( t < t2 ) goto while_ff;
    goto do_begin;
    
while_ff:
    u1 -= 1;
    u4 -= 2;
    u3 = u1 + u4;

for_end:
    u4 += 1;
    u3 %= u4;
    goto for_beg;
    
for_ff:
    t = u4 - u2;
    t2 = u2 + u3;
    t *= 5;
    t2 /= 6;
    t += t2;
    t -= u1;
    
    return 0;
}

问题与解答 #

1. 除了逐行验证，是否应该使用调试工具？ #

必须用调试工具，逐行检查极易遗漏循环时序、分支判断、变量修改顺序这类细节。推荐方式：

• 用GDB或IDE内置调试器，给两份代码输入相同测试用例，在循环入口、分支判断前、变量修改后设置断点，跟踪每一步的变量值，对比两份代码的执行流程和变量状态是否完全一致。
• 配合printf打印关键变量，但要选对时机：比如在每次循环迭代前后打印终止条件的相关变量（如i2、i3-i1、u2、u1），而非仅打印单个变量。

2. 打印u1仍陷入循环的问题 #

先排查两份代码的核心逻辑差异，这是循环异常的根本原因：

• for循环终止条件逻辑不一致：Style 1每次循环都会重新计算i3-i1，但Style 2中t = i3 - i1仅在循环前赋值一次，后续i3和i1被修改后t不会更新，导致循环判断条件完全偏离。
• do-while循环逻辑错误：Style 1中u4 = (u4 << 2) & ~0x04，但Style 2拆分为u4 = u4 << 2; u4 = ~0x04，直接将u4赋值为~0x04（无符号下为极大值），导致do-while循环仅执行一次，与Style 1逻辑完全不符。
• 输入格式错误：Style 2中scanf("%d", &u1)，u1是unsigned类型，应使用%u格式符，否则输入负数会触发未定义行为。

定位死循环的具体操作：在循环入口打印终止条件的所有变量值，看为何终止条件一直不满足。比如在Style 1的for循环开头添加：

printf("Loop check: i2=%d, i3-i1=%d, u2=%u, u1=%u\n", i2, i3-i1, u2, u1);

在Style 2的for_beg:标签后添加：

printf("Loop check: i2=%d, t=%d, u2=%u, u1=%u\n", i2, t, u2, u1);

对比两份代码的输出，可快速定位循环条件的差异。

内容的提问来源于stack exchange，提问作者ditex