[dnautics]

as someone building an analyzer for zig, if you sent something like this through the system im building, it would get handled by Zig's optional type tagging; but lets say you did "free" (so your result is half freed, half not freed): it would get rejected because both branches produce inconsistent type refinements, you don't have to solve the halting problem, just analyze all possible branches and seek convergence.

[dwattttt]

Rust is the poster child for these complaints, but this is a great example of "the language rejects a valid program". Not all things that can be expressed in C are good ideas!

This is "valid" C, but I wholly support checking tools that reject it.

[dnautics]

exactly! "guaranteeing the safety of C" sir what did you think that meant, sprinkling magic fairy dust to make it work!!?

[dnautics]

i made a quip and realized that's not a bad description of what fil-c does

[throwaway17_17]

Are you implying that Fil-C has this sort of reaction to people confused about why it does certain things in the name of safety, or are you saying Fil-C is just sprinkling magic fairy dust on C and declaring it safe?

[dnautics]

i like fil-c, so i would say "fil c sprinkles magic fairy dust on C and makes it safe (at the cost of perf and elevated risk of crashing)

[SkiFire13]

> just analyze all possible branches and seek convergence.

This sounds like a very simple form of abstract interpretation, how do you handle the issues it generally brings?

For example if after one branch you don't converge, but after two you do, do you accept that? What if this requires remembering the relationship between variables? How do you represent these relationships?

Historically this has been a tradeoff between representing the state space with high or perfect precision, which however can require an exponential amount of memory/calculations, or approximate them with an abstract domain, which however tend to lose precision after performing certain operations.

Add dynamically sized values (e.g. arrays) and loops/recursion and now you also need to simulate a possibly unbounded number of iterations.

[dnautics]

> For example if after one branch you don't converge, but after two you do, do you accept that?

you should refactor so that it's representable.

> Add dynamically sized values (e.g. arrays) and loops/recursion and now you also need to simulate a possibly unbounded number of iterations.

regions are hard. You kinda have to reject regions that are not uniform. loops you can find a fixpoint for.