dhekir

A few corrections and counterpoints:

- Frama-C is developed by CEA (French nuclear research agency; Inria participated in the beginning of the project, and is still a partner, but development has always been led by CEA);

- Your first-order of approximation is a bit severe; there are formal methods groups within large companies, such as Airbus using Astrée, Frama-C, and CompCet; Framatome (French nuclear reactor business) using Astrée; EDF (French electrical company) using Frama-C; plus several railway companies using formal methods such as B; and NASA, Thales, Scania... It's peanuts compared to the amount of money being poured into blockchains, AI, and the latest hype, but formal methods are used in some industries.

Overall, I agree with you: it's not the best time investment for many SWEs, but if you like maths, formal methods do provide some satisfaction and long-term hope that we'll stop patching bugs and rewriting things all the time, and build some longer-lasting software.

OP could be referring to Raynaud syndrome (https://en.wikipedia.org/wiki/Raynaud_syndrome). It's not sure tea helps in such cases.

After moving to a newly-finished building, I realized most companies didn't have up-to-date databases and some forms prevented me from correcting the "mis-corrected" addresses. Missed a few deliveries during the first few months/years.

On the other hand, having lived in a country where such databases were notoriously unreliable, such automated processing didn't exist, so I didn't encounter that problem.

Sometimes, having something work "way too well" can lead people to believe it's perfect, and enforce it too strictly.

Every single laptop my company bought me in the last 10 years (3+) had kernel/driver issues, especially with Ubuntu, since the kernel version was usually lower than that from other distros, like Fedora.

This includes mostly graphics driver issues (either simply Nvidia, or hybrids, or some exotic protocols such as DisplayLink), but also touchpad, power/suspend issues (e.g. wake-up failure), lack of fingerprint or smartcard reader drivers... Without mentioning certain manufacturers forcing you to use Windows simply to update docking station firmware drivers (like Dell does).

I still favor Linux whenever I can, but there is a real issue in several models, especially bleeding-edge powerful laptops from brands favored by businesses. Linux certification does improve things, but it often omits "optional" components such as fingerprint readers.

Overall, about 1-2 years after the new laptop model has been released, almost everything works fine, but when you're among the first users, some amount of time will be spent in forums trying to find solutions and workarounds for such issues.

This echoes some vibes of Neal Stephenson's Zodiac. Replace Boston with The Bay, PCBs with VOCs, and fast-forward some 30 years, and there you have it. If only we could learn from past mistakes...

Fixing the Ctrl+Q issue is great, but I still think extensions such as Form History Control are essential for all other situations. I'd very much appreciate if Mozilla could vet it for security; I'm always afraid of some developer selling out or being hacked and a future update introducing a backdoor.

Frama-C is a framework for code analysis. It can help proving code with the aid of ACSL (JML-like notation for C contracts).

But I agree that C is not the best language for writing critical code.

Can you get a long term visa without any job affiliations? I'm not sure that simply having the money is sufficient reason for an European country to give you a long-term visa (> 1 year), depending on which country you come from.

Also, some countries have a "negative privilege" situation, where even if you try to get a low-wage job, you'll have less priority than others, or your employer will need to pay an extra fee to be able to hire you. Many will resort to illegal employment to avoid that.

And do not forget issues about guarantors: some places are really strict about proving you have the money, and simply making a 1-year rent deposit in advance is not enough.

Overall, even when having the money, some people don't have the "privilege" of being able to spend it as they please, in the country of their preference.

Genius! Good to know it exists, if I need it one day.

For now, I tried patching the timestamp in the binary as suggested by jtvjan, since I saw it before your post. It works, so I'll stick with it for now. But I'll be sure to try this RunAsDate when I need something similar in the future.

Thanks a lot! The page you linked did work; I had to copy the Flash folder elsewhere, used a hex editor to find the timestamp in my Flash.ocx file, then I renamed the original folder to Flash.bak and copied the modified one in its place, and my application works again!

Indeed, the laptop has been disconnected for days. I (or, more precisely, Windows) inadvertently updated to a more recent Flash version containing the "time bomb", so now the application simply checks the system date and decides whether to block it or not.

If I could "sandbox the clock" for this specific application, that might work, but I don't think that it is possible.

I have an old Windows offline desktop application (from circa 2003) that has an embedded Flash component which is necessary for it to run properly. It simply stopped working this morning on my Windows 10.

Resetting the date to yesterday works, but I'd like to avoid it if possible.

Standalone flash players (such as Newgrounds') do not work, since the desktop application is the one who actually runs the Flash component, and I cannot control it directly.

I tried uninstalling Flash and reinstalling an older version, without success: it seems to be using an ActiveX component which I cannot overwrite, since the old installer says "You already have a newer version". Windows does not allow me uninstalling it manually (it's "part of the system", and apparently the only Windows Update KB which allows it to be uninstalled, prevents you from installing any other Flash version), and I tried manually searching for registry keys, but there are several and I need to change permissions, etc.

So, I'm afraid I'll have to run an emulator such as PCem, with an older Windows inside, whose date is set to a distant past, so that my app will simply keep working as usual. I'd appreciate if there are simpler solutions.

OCaml is good for handling abstract syntax trees (strong typing, pattern matching) and its mix of imperative and functional programming don't require using borrow-checker nor monads. You can also consider Reason, if you prefer a more C-like syntax.

Would you mind telling some of the kinds of checks the Clang tools do not perform? I wonder if they are mostly syntactic or if they need dataflow analyses. (That said, Polyspace has 2 tools now, Bug Finder and Code Prover, whose applications are somewhat different.)

Too bad it's not open source, but will some of the generated programs be?

Also, would you mind comparing it to Csmith (https://embed.cs.utah.edu/csmith/)?

I also found this "amalgamate" script on GitHub, intended to allow creating such amalgamations from C/C++ projects:

https://github.com/rindeal/Amalgamate

Which seems interesting, however when I tried the FreeType example, there seemed to be some preprocessing issue, such that some function definitions are conditionally excluded even though they are called later. I didn't have the time to find out if this was an issue in the original code or if the amalgamation script introduced it.

In any case, such single-C programs are very useful for quickly testing tools, so having more of them would be great.

I had never heard of LSIF. Its webpage says it intends to "define a standard format for language servers or other programming tools to dump their knowledge about a workspace". SARIF being targeted towards static analysis tools results, it seems more straightforward to support it both for producing results and for reading them.

To be honest, since both formats are at least partially developed by Microsoft, they might have some common people behind them, but as a user and producer of static analysis tools, I'd prefer to have a single standard. SARIF is already standardized and gaining traction, so it seems the better choice for now.

It would be useful to list which tools support the SARIF standardized format (https://sarifweb.azurewebsites.net/).

I'm at work and not allowed to read active patents.

Is that related to legal issues (as in, if you don't read patents, there's less chance that you'll end up being prosecuted if you accidentally implement something similar)?

ACSL (https://en.wikipedia.org/wiki/ANSI/ISO_C_Specification_Langu...) for C, which is based on JML (https://en.wikipedia.org/wiki/Java_Modeling_Language) for Java, both use 'requires' for preconditions, 'ensures' for postconditions, and 'invariant' for invariants. Some invariants are also written as assertions ('assert').

It always happens for me when accessing a Linux machine remotely. I can't find a screenshot now, so the next time I do it, I'll take one. It seems to be a security measure, to prevent someone from sharing remote access and then forgetting about it afterwards, but it makes for terrible usability.

But for remote control, it stops after every few minutes, asking the "controlled" user to click on a button to continue. Not so practical in a few situations.

It stopped working earlier this year, due to OAuth API changes by Google, if I'm not mistaken. Or did you manage to get it working?

Any backup recommendations? Gmvault stopped working earlier this year, and for multi-gigabyte accounts via a connection that is prone to get interrupted every once in a while, I couldn't find anything that seemed as simple and robust (Gmvault allowed incremental backups, tolerated disconnections, ...).

I used to walk around taking pictures and memorizing some key points to later upload the data from JOSM, but it was very time-consuming and a lot of time was spent matching the aerial view with my street-level pictures.

So I started trying to use Vespucci from my Android, but it's interface is really sophisticated and not ideal for "lightweight" work, such as adding POIs (when the streets, paths and shapes are already in place).

I also liked a lot Street Complete, but it does not allow _adding_ new POIs, just completing existing ones.

Finally, a Frenchman developed OSM Go! (https://play.google.com/store/apps/details?id=fr.dogeo.osmgo..., open source on Github, but not yet available on F-Droid), which is the sweet spot for me: not as powerful as Vespucci, but much easier to use for adding/updating POIs. It has recently been translated into English, and though the UI is not perfect, it greatly improved the ease of contribution.

So now I am much more inclined to, when walking around somewhere with incomplete mapping, simply stop for a few seconds, add some missing data (wheelchair accessibility, opening hours, or a minor POI such as drinking water or even trash basket), and keep on walking. No extra homework required!

The amount of effort the community devotes to such apps and to OSM in general is incredible and contagious!

Not only Infer, but other static analyzers would also be useful.

Hopefully Software Heritage (https://www.softwareheritage.org) will help with that.

The author's blog says:

All site content © Paul Reiffer 2019 and may not be used without permission

And Petapixel's post credits him, and includes in the end:

About the author: (...) This article was also published here [link to author's blog].

So, I assume it has been authorized by the author? Does he prefer to have a link to his own blog directly?

Unfortunately seems inaccessible, at least in France: "Access Denied - Sucuri Website Firewall - Block reason: Access from your Country was disabled by the administrator."

Receiving unintended funds can have all kinds of unintended consequences, including related to law enforcement.

In his case, he just got suspended and asked to provide documents he is physically unable to produce (contrary to presumption of innocence).

the next day, and after almost two weeks since the refund to place (but only one day after the long phone discussion) my account was blocked as "suspicious" activity and in order to unblock it I will have to provide original product receipts of the product I was "selling", something that I do not have as I do not even know what I was selling!

Why should they work for Google for free? Google Maps is a business and should pay for the accuracy of its data. Or OP can contribute to OpenstreetMap to the point it will contain enough and accurate data to be a preferred source for this kind of information. It won't automatically solve the problem with scammers, but with several users policing the accuracy of the data, instead of only Google being the gatekeeper, several solutions become possible. For instance, the Wikipedia model.